Ssrtacticals (p.rocq-runtime.9.3.0.doc.ssreflect_plugin.Ssreflect

Source

val tclSEQAT : 
  Ltac_plugin.Tacinterp.interp_sign ->
  Ltac_plugin.Tacarg.tacvalue ->
  Ssrast.ssrdir ->
  (int Locus.or_var
   * (('a * Ltac_plugin.Tacarg.tacvalue option list)
      * Ltac_plugin.Tacarg.tacvalue option)) ->
  unit Proofview.tactic

Source

val tclCLAUSES : 
  unit Proofview.tactic ->
  ((Ssrast.ssrhyps
    * ((Ssrast.ssrhyp_or_id * string)
       * Ssrmatching_plugin.Ssrmatching.cpattern option)
        option)
     list
   * Ssrast.ssrclseq) ->
  unit Proofview.tactic

Source

val hinttac : 
  Ltac_plugin.Tacinterp.interp_sign ->
  bool ->
  (bool * Ltac_plugin.Tacarg.tacvalue option list) ->
  unit Proofview.tactic

Source

val ssrdotac : 
  Ltac_plugin.Tacinterp.interp_sign ->
  (((int Locus.or_var * Ssrast.ssrmmod)
    * (bool * Ltac_plugin.Tacarg.tacvalue option list))
   * ((Ssrast.ssrhyps
       * ((Ssrast.ssrhyp_or_id * string)
          * Ssrmatching_plugin.Ssrmatching.cpattern option)
           option)
        list
      * Ssrast.ssrclseq)) ->
  unit Proofview.tactic