redeplacement des var. ex. dans kernel :-)

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

1 files changed, 48 insertions, 0 deletions

diff --git a/kernel/evd.mli b/kernel/evd.mli
new file mode 100644
index 000000000..8063f42b0
--- /dev/null
+++ b/kernel/evd.mli
@@ -0,0 +1,48 @@
+
+(* $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
+