Module Ltac2_plugin.Tac2match
type context= Constr_matching.contexttype match_pattern=|MatchPattern of Pattern.constr_pattern|MatchContext of Pattern.constr_patterntype match_context_hyps= match_pattern option * match_patterntype match_rule= match_context_hyps list * match_pattern
val match_goal : Environ.env -> Evd.evar_map -> EConstr.constr -> rev:bool -> match_rule -> ((Names.Id.t * context option option * context option) list * context option * Ltac_pretype.patvar_map) Proofview.tactic