Module `Ssreflect_plugin.Ssrtacticals`

val tclSEQAT : Ltac_plugin.Tacinterp.interp_sign -> Ltac_plugin.Tacinterp.Value.t -> Ssrast.ssrdir -> (int Locus.or_var * (('a * Ltac_plugin.Tacinterp.Value.t option list) * Ltac_plugin.Tacinterp.Value.t option)) -> unit Proofview.tactic
val tclCLAUSES : unit Proofview.tactic -> ((Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq) -> unit Proofview.tactic
val hinttac : Ltac_plugin.Tacinterp.interp_sign -> bool -> (bool * Ltac_plugin.Tacinterp.Value.t option list) -> unit Proofview.tactic
val ssrdotac : Ltac_plugin.Tacinterp.interp_sign -> (((int Locus.or_var * Ssrast.ssrmmod) * (bool * Ltac_plugin.Tacinterp.Value.t option list)) * ((Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq)) -> unit Proofview.tactic