From 42537fb14ea0f3aa8ee761dc66bf5c987de8068d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 1 Mar 2005 10:57:34 +0000
Subject: Code mort

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

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b0aed65e17..a49d8540b9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -140,12 +140,6 @@ let meta_instance env b =
 
 let nf_meta env c = meta_instance env (mk_freelisted c)
 
-let meta_type env mv =
-  let ty =
-    try meta_ftype env mv
-    with Not_found -> error ("unknown meta ?"^string_of_int mv) in
-  meta_instance env ty
-
 (**********************)
 (* Creating new evars *)
 (**********************)
@@ -283,6 +277,7 @@ let real_clean env isevars ev args rhs =
  	 if i<=k then t
  	 else (try List.assoc (mkRel (i-k)) subst with Not_found -> t)
       | Evar (ev,args) ->
+
 	  let args' = Array.map (subs k) args in
 	  if need_restriction !evd args' then
             if Evd.is_defined_evar !evd (ev,args) then 
-- 
cgit v1.2.3