From b3081e0906e7096e5b1aef3d5a865881d660c917 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 27 Apr 2016 22:13:02 +0200 Subject: Revert "When interpreting "match goal with ... end" in ltac, expand evars by" This reverts commit 7e613daf7c71a4180725bddb40151c2b5a6348f4. --- pretyping/constr_matching.ml | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'pretyping/constr_matching.ml') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 52c132266..4fb411202 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 sigma n (ids, m as x) (names, terms as subst) = +let constrain 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' && Evarutil.eq_constr_univs_test sigma sigma m m' then subst + if List.equal Id.equal ids ids' && eq_constr 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 sigma allow_bound_rels ctx n cT subst = +let merge_binding allow_bound_rels ctx n cT subst = let c = match ctx with | [] -> (* Optimization *) ([], cT) @@ -150,7 +150,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = ([], lift (- depth) cT) else raise PatternMatchingFailure in - constrain sigma n c subst + constrain n c subst let matches_core env sigma convert allow_partial_app allow_bound_rels (binding_vars,pat) c = @@ -168,7 +168,6 @@ 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 @@ -180,11 +179,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 sigma n ([], build_lambda relargs ctx cT) subst + constrain n ([], build_lambda relargs ctx cT) subst else raise PatternMatchingFailure - | PMeta (Some n), m -> merge_binding sigma allow_bound_rels ctx n cT subst + | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst | PMeta None, m -> subst @@ -215,7 +214,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let subst = match meta with | None -> subst - | Some n -> merge_binding sigma allow_bound_rels ctx n c subst in + | Some n -> merge_binding 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 @@ -305,8 +304,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 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 + | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst + | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst | _ -> raise PatternMatchingFailure in -- cgit v1.2.3