Code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6787 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 1 insertions, 20 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b0aed65e1..a49d8540b 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 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c5839ca7d..b032395e1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -329,19 +329,6 @@ let vernac_import export refl =
   List.iter import refl;
   Lib.add_frozen_state ()
 
-(*  else
-    let import (loc,qid) = 
-      try
-	let mp = Nametab.locate_module qid in
-	  Declaremods.import_module mp
-      with Not_found ->
-	user_err_loc
-        (loc,"vernac_import",
-	 str ((string_of_qualid qid)^" is not a module"))
-    in
-      List.iter import qidl;
-*)
-
 let vernac_declare_module export id binders_ast mty_ast_o = 
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
@@ -463,7 +450,6 @@ let vernac_record struc binders sort nameopt cfs =
   (* Sections *)
 
 let vernac_begin_section = Lib.open_section
-
 let vernac_end_section = Lib.close_section
 
 let vernac_end_segment id =