deplacements des var. ex. hors du noyau

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

1 files changed, 0 insertions, 48 deletions

diff --git a/kernel/evd.mli b/kernel/evd.mli
deleted file mode 100644
index 696fcdd3b3..0000000000
--- a/kernel/evd.mli
+++ /dev/null
@@ -1,48 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-open Term
-open Sign
-(*i*)
-
-(* The type of mappings for existential variables.
-   The keys are section paths and the associated information is a record
-   containing the type of the evar ([concl]), the signature under which 
-   it was introduced ([hyps]), its definition ([body]) and any other 
-   possible information if necessary ([info]).
-*)
-
-type evar_body =
-  | EVAR_EMPTY 
-  | EVAR_DEFINED of constr
-
-type 'a evar_info = {
-  evar_concl : typed_type;
-  evar_hyps  : typed_type signature;
-  evar_body  : evar_body;
-  evar_info  : 'a option }
-
-type 'a evar_map
-
-val dom    : 'a evar_map -> section_path list
-val map    : 'a evar_map -> section_path -> 'a evar_info
-val rmv    : 'a evar_map -> section_path -> 'a evar_map
-val remap  : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
-val in_dom : 'a evar_map -> section_path -> bool
-val toList : 'a evar_map -> (section_path * 'a evar_info) list
-
-val mt_evd : 'a evar_map
-val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
-val add_noinfo : 
-  'a evar_map -> section_path -> typed_type signature -> typed_type 
-    -> 'a evar_map
-
-val define : 'a evar_map -> section_path -> constr -> 'a evar_map
-
-val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
-val is_evar : 'a evar_map -> section_path -> bool
-
-val is_defined : 'a evar_map -> section_path -> bool
-