GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

1 files changed, 0 insertions, 57 deletions

diff --git a/kernel/evd.mli b/kernel/evd.mli
deleted file mode 100644
index f6192c7e50..0000000000
--- a/kernel/evd.mli
+++ /dev/null
@@ -1,57 +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*)
-
-(*i*)
-open Names
-open Term
-open Sign
-(*i*)
-
-(* The type of mappings for existential variables.
-   The keys are integers and the associated information is a record
-   containing the type of the evar ([evar_concl]), the context under which 
-   it was introduced ([evar_hyps]) and its definition ([evar_body]). 
-   [evar_info] is used to add any other kind of information. *)
-
-type evar = int
-
-type evar_body =
-  | Evar_empty 
-  | Evar_defined of constr
-
-type 'a evar_info = {
-  evar_concl : constr;
-  evar_hyps : named_context;
-  evar_body : evar_body;
-  evar_info : 'a option }
-
-type 'a evar_map
-
-val empty : 'a evar_map
-
-val add : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
-
-val dom : 'a evar_map -> evar list
-val map : 'a evar_map -> evar -> 'a evar_info
-val rmv : 'a evar_map -> evar -> 'a evar_map
-val remap : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
-val in_dom : 'a evar_map -> evar -> bool
-val to_list : 'a evar_map -> (evar * 'a evar_info) list
-
-val define : 'a evar_map -> evar -> constr -> 'a evar_map
-
-val non_instantiated : 'a evar_map -> (evar * 'a evar_info) list
-val is_evar : 'a evar_map -> evar -> bool
-
-val is_defined : 'a evar_map -> evar -> bool
-
-val evar_body : 'a evar_info -> evar_body
-
-val id_of_existential : evar -> identifier