From 86af14b5e0b813df0949659bb77f8e7d88bcd1aa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 11 Dec 2014 19:06:12 +0100 Subject: Commit not ready. Sorry. Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags." This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968. --- pretyping/unification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 40b81dd4c6..a53240a1cf 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1368,7 +1368,7 @@ let w_unify_core_0 env evd with_types cv_pb flags m n = let (mc1,evd') = retract_coercible_metas evd in let (sigma,ms,es) = check_types env (set_flags_for_type flags.core_unify_flags) (evd,mc1,[]) m n in let subst2 = - unify_0_with_initial_metas (sigma,ms,es) false env cv_pb + unify_0_with_initial_metas (evd',ms,es) false env cv_pb flags.core_unify_flags m n in let evd = w_merge env with_types flags.merge_unify_flags subst2 in -- cgit v1.2.3