From aaf2ca06f7f0ae5e7be30aaf5c5dcd6677bfb016 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Oct 2000 15:36:27 +0000
Subject: Chasse au Cast de Cast

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

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5ef2d60357..726042c356 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -441,7 +441,7 @@ let clenv_cast_meta clenv =
 	     match Intmap.find mv clenv.env with
                | Cltyp b ->
 		   let b' = clenv_instance clenv b in 
-		   if occur_meta b' then u else mkCast (u, b')
+		   if occur_meta b' then u else mkCast (mkMeta mv, b')
 	       | Clval(_) -> u
 	   with Not_found -> 
 	     u)
-- 
cgit v1.2.3