From 056c60125b0052cebaa9a2a6e80005c2c7c85366 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 3 Apr 2001 08:07:48 +0000
Subject: ménage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1521 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/close_env.ml  | 18 ------------------
 contrib/extraction/close_env.mli | 16 ----------------
 contrib/extraction/rename.mli    | 21 ---------------------
 3 files changed, 55 deletions(-)
 delete mode 100644 contrib/extraction/close_env.ml
 delete mode 100644 contrib/extraction/close_env.mli
 delete mode 100644 contrib/extraction/rename.mli

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
-- 
cgit v1.2.3