From 0962a284f57b18a6f40f68875d386bc479285bc4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 3 Aug 2011 14:25:55 +0000
Subject: Fix nf_evars_undefined

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14382 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 49a7b3a266..ab14495f62 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -58,7 +58,6 @@ let nf_evar_info evc info =
     evar_body = match info.evar_body with
       | Evar_empty -> Evar_empty
       | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
-
 let nf_evars evm =
   Evd.fold
     (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
@@ -67,7 +66,7 @@ let nf_evars evm =
 let nf_evars_undefined evm =
   Evd.fold_undefined
     (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
-    evm Evd.empty
+    evm (defined_evars evm)
 
 let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
 let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd
-- 
cgit v1.2.3