diff options
Diffstat (limited to 'plugins/ltac/tactic_matching.ml')
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index e87951dd7..6bf9215e0 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -306,9 +306,9 @@ module PatternMatching (E:StaticEnvironment) = struct [pat] is [Hyp _] or [Def _]. *) let hyp_match pat hyps = match pat with - | Hyp ((_,hypname),typepat) -> + | Hyp ({CAst.v=hypname},typepat) -> hyp_match_type hypname typepat hyps - | Def ((_,hypname),bodypat,typepat) -> + | Def ({CAst.v=hypname},bodypat,typepat) -> hyp_match_body_and_type hypname bodypat typepat hyps (** [hyp_pattern_list_match pats hyps lhs], matches the list of |