3 files changed, 0 insertions, 55 deletions
diff --git a/contrib/extraction/close_env.ml b/contrib/extraction/close_env.ml
deleted file mode 100644
index ab303b0947..0000000000
--- a/contrib/extraction/close_env.ml
+++ /dev/null
@@ -1,18 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-open Names
-open Term
-
-let close gl =
-  failwith "todo"
-
-let module_env m = 
-  failwith "todo"
diff --git a/contrib/extraction/close_env.mli b/contrib/extraction/close_env.mli
deleted file mode 100644
index bf6940d1cc..0000000000
--- a/contrib/extraction/close_env.mli
+++ /dev/null
@@ -1,16 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-open Names
-open Term
-
-val close : global_reference list -> global_reference list
-
-val module_env : identifier -> global_reference list
diff --git a/contrib/extraction/rename.mli b/contrib/extraction/rename.mli
deleted file mode 100644
index 9ed0c475ca..0000000000
--- a/contrib/extraction/rename.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-
-(* Renaming issues. *)
-
-open Names
-open Term
-open Miniml
-
-type renaming_function = Idset.t -> name -> identifier
-
-module type Renaming = sig
-  val rename_type_parameter : renaming_function
-  val rename_type : renaming_function
-  val rename_term : renaming_function
-  val rename_global_type : renaming_function
-  val rename_global_constructor : renaming_function
-  val rename_global_term : renaming_function
-end
-
-module Make : functor(R : Renaming) -> sig
-
-end