From e1e84686f5f5a57b57c19f350ab5d4ffd1b9c91f Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 19 Feb 2002 10:19:31 +0000
Subject: Le type des evars transformees en meta n'etait pas normalise, et des
 Evars definies y apparaissait

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8e9e0278ea..1d69a14ae9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -483,7 +483,8 @@ let check_evars fail_evar initial_sigma sigma c =
 		(str"There is an unknown subterm I cannot solve")
 	    else (* try to avoid duplication *)
               (if not (List.exists (fun (k',_) -> k=k') !metamap) then
-	        metamap := (k, existential_type sigma k) :: !metamap))
+	        metamap :=
+                (k, nf_evar sigma (existential_type sigma k)) :: !metamap))
       | _ -> iter_constr proc_rec c      
   in
   (proc_rec c; !metamap)
-- 
cgit v1.2.3