From a87dd193cb6a31ba528626e34a1bbb9b58c14f2e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 Dec 2014 18:45:54 +0100
Subject: New try on Fixing an evar_map bug revealed by commit 603b66f81 on
 unification flags (see also temporary revert in d083200ae5b).

---
 pretyping/unification.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7ea074b748..5f3ea7a98d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1367,9 +1367,9 @@ let try_resolve_typeclasses env evd flag m n =
 
 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 (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 (evd',ms,es) false env cv_pb
+     unify_0_with_initial_metas (sigma,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