Module Ltac2_plugin.Tac2match
type context
= Constr_matching.context
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