Ltac2_plugin.Tac2matchThis file extends Matching with the main logic for Ltac2 match goal.
type context = Constr_matching.contexttype match_pattern = | MatchPattern of Pattern.constr_pattern |
| MatchContext of Pattern.constr_pattern |
type match_context_hyps = match_pattern option * match_patterntype match_rule = match_context_hyps list * match_patternval 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