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