Ssrfwd (p.coq-core.8.17.1.doc.ssreflect_plugin.Ssreflect

Source

val ssrsettac : 
  Names.Id.t ->
  ((Ssrast.ssrfwdfmt
    * (Ssrmatching_plugin.Ssrmatching.cpattern * Ssrast.ast_closure_term option))
   * Ssrast.ssrdocc) ->
  unit Proofview.tactic

Source

val ssrposetac : 
  (Names.Id.t * (Ssrast.ssrfwdfmt * Ssrast.ast_closure_term)) ->
  unit Proofview.tactic

Source

val havetac : 
  Ssrast.ist ->
  (bool
   * ((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats)
       * Ssrast.ssripats)
      * (((Ssrast.ssrfwdkind * 'a) * Ssrast.ast_closure_term)
         * (bool * Ltac_plugin.Tacinterp.Value.t option list)))) ->
  bool ->
  bool ->
  unit Proofview.tactic

Sourcetype cut_kind =

| Have
| HaveTransp
| Suff

Sourceval basecuttac : cut_kind -> EConstr.t -> unit Proofview.tactic

Sourceval basesufftac : EConstr.t -> unit Proofview.tactic

Source

val wlogtac : 
  Ltac_plugin.Tacinterp.interp_sign ->
  (((Ssrast.ssrclear option * Ssrast.ssripats) * 'a) * 'b) ->
  ((Ssrast.ssrhyps
    * ((Ssrast.ssrhyp_or_id * string)
       * Ssrmatching_plugin.Ssrmatching.cpattern option)
        option)
     list
   * ('c * Ssrast.ast_closure_term)) ->
  Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
  bool ->
  [< `Gen of Names.Id.t option option | `NoGen NoGen ] ->
  unit Proofview.tactic

Source

val sufftac : 
  Ssrast.ist ->
  ((((Ssrast.ssrclear option * Ssrast.ssripats) * Ssrast.ssripat list)
    * Ssrast.ssripat list)
   * (('a * Ssrast.ast_closure_term)
      * (bool * Ltac_plugin.Tacinterp.Value.t option list))) ->
  unit Proofview.tactic

Source

val undertac : 
  ?pad_intro:bool ->
  Ltac_plugin.Tacinterp.interp_sign ->
  Ssrast.ssripats option ->
  Ssrequality.ssrrwarg ->
  Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
  unit Proofview.tactic

Sourceval overtac : unit Proofview.tactic