diff options
| -rw-r--r-- | ltac/tacinterp.ml | 4 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 19 |
2 files changed, 13 insertions, 10 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index e8dee7a001..b742bb328d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1530,7 +1530,9 @@ and interp_match ist lz constr lmr = (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = - Ftactic.nf_enter { enter = begin fun gl -> + Ftactic.enter { enter = begin fun gl -> + (* Because match_goal will lazily whd_evar when necessary *) + let gl = Proofview.Goal.assume gl in let sigma = project gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 4fb4112022..52c1322669 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -56,10 +56,10 @@ let warn_bound_meta name = let warn_bound_bound name = msg_warning (str "Collision between bound variables of name " ++ pr_id name) -let constrain n (ids, m as x) (names, terms as subst) = +let constrain sigma n (ids, m as x) (names, terms as subst) = try let (ids', m') = Id.Map.find n terms in - if List.equal Id.equal ids ids' && eq_constr m m' then subst + if List.equal Id.equal ids ids' && Evarutil.eq_constr_univs_test sigma sigma m m' then subst else raise PatternMatchingFailure with Not_found -> let () = if Id.Map.mem n names then warn_bound_meta n in @@ -131,7 +131,7 @@ let make_renaming ids = function end | _ -> dummy_constr -let merge_binding allow_bound_rels ctx n cT subst = +let merge_binding sigma allow_bound_rels ctx n cT subst = let c = match ctx with | [] -> (* Optimization *) ([], cT) @@ -150,7 +150,7 @@ let merge_binding allow_bound_rels ctx n cT subst = ([], lift (- depth) cT) else raise PatternMatchingFailure in - constrain n c subst + constrain sigma n c subst let matches_core env sigma convert allow_partial_app allow_bound_rels (binding_vars,pat) c = @@ -168,6 +168,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels in let rec sorec ctx env subst p t = let cT = strip_outer_cast t in + let cT = whd_evar sigma cT in match p,kind_of_term cT with | PSoApp (n,args),m -> let fold (ans, seen) = function @@ -179,11 +180,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in let frels = free_rels cT in if Int.Set.subset frels relset then - constrain n ([], build_lambda relargs ctx cT) subst + constrain sigma n ([], build_lambda relargs ctx cT) subst else raise PatternMatchingFailure - | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst + | PMeta (Some n), m -> merge_binding sigma allow_bound_rels ctx n cT subst | PMeta None, m -> subst @@ -214,7 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let subst = match meta with | None -> subst - | Some n -> merge_binding allow_bound_rels ctx n c subst in + | Some n -> merge_binding sigma allow_bound_rels ctx n c subst in Array.fold_left2 (sorec ctx env) subst args1 args22 else (* Might be a projection on the right *) match kind_of_term c2 with @@ -304,8 +305,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in List.fold_left chk_branch chk_head br1 - | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst - | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst + | PFix c1, Fix _ when Evarutil.eq_constr_univs_test sigma sigma (mkFix c1) cT -> subst + | PCoFix c1, CoFix _ when Evarutil.eq_constr_univs_test sigma sigma (mkCoFix c1) cT -> subst | _ -> raise PatternMatchingFailure in |