From 9fad5317634c476fdb073c7dfa3ea81b6607d41f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Mar 2000 00:05:37 +0000
Subject: Remplacement plain_instance en instance qui n'a plus besoin de env

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

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5973e22e97..0084e96f3f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -429,7 +429,7 @@ let clenv_val_of clenv mv =
       (match Intmap.find mv clenv.env with
 	 | Cltyp _ -> DOP0(Meta mv)
 	 | Clval(b,_) ->
-	     plain_instance (List.map (fun mv' -> (mv',valrec mv')) 
+	     instance (List.map (fun mv' -> (mv',valrec mv')) 
 			       (Intset.elements b.freemetas)) b.rebus)
     with Not_found -> 
       DOP0(Meta mv)
@@ -441,7 +441,7 @@ let clenv_instance clenv b =
     List.map 
       (fun mv -> (mv,clenv_val_of clenv mv)) (Intset.elements b.freemetas)
   in 
-  plain_instance c_sigma b.rebus
+  instance c_sigma b.rebus
     
 let clenv_instance_term clenv c =
   clenv_instance clenv (mk_freelisted c)
-- 
cgit v1.2.3