From 9e1bc9aa4e2963a11ffd9a286a9e6319fe1cb5c6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 13:04:33 +0000
Subject: C'est trop compliqué de mettre à jour les types du metamap en passant
 sous les lieurs, plus simple de garder le type avec un cast (cf bug #889)

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

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c199eb0083..763bfa54d9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -109,7 +109,7 @@ let exist_to_meta sigma (emap, c) =
     let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
     let n = new_meta() in
     metamap := (n, ty) :: !metamap;
-    mkMeta n in
+    mkCast (mkMeta n, ty) in
   let rec replace c =
     match kind_of_term c with
         Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
-- 
cgit v1.2.3