Module Ltac2_plugin.Tac2match

type context = EConstr.t
type match_pattern =
| MatchPattern of Pattern.constr_pattern
| MatchContext of Pattern.constr_pattern
type match_context_hyps = match_pattern

TODO: handle definitions

type 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) list * context option * Ltac_pretype.patvar_map) Proofview.tactic