From d083200ae5b391ceffaa0329a8e3a334036c7968 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 11 Dec 2014 14:34:31 +0100
Subject: Fixing an evar_map bug revealed by commit 603b66f81 on unification
 flags.

This fixes current failure of RelationAlgebra.
---
 pretyping/unification.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a53240a1cf..40b81dd4c6 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 (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