premiere reorganisation de l\'unification

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

1 files changed, 51 insertions, 0 deletions

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 567097d0d..3f9eaa5fa 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -54,3 +54,54 @@ val evar_body : evar_info -> evar_body
 
 val string_of_existential : evar -> string
 val existential_of_int : int -> evar
+
+(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+    no body and [Not_found] if it does not exist in [sigma] *)
+
+exception NotInstantiatedEvar
+val existential_value : evar_map -> existential -> constr
+val existential_type : evar_map -> existential -> types
+val existential_opt_value : evar_map -> existential -> constr option
+
+(*************************)
+(* The type constructor ['a sigma] adds an evar map to an object of
+  type ['a] *)
+type 'a sigma = {
+  it : 'a ;
+  sigma : evar_map}
+
+val sig_it  : 'a sigma -> 'a
+val sig_sig : 'a sigma -> evar_map
+
+(*************************)
+(* Meta map *)
+
+module Metaset : Set.S with type elt = metavariable
+
+val meta_exists : (metavariable -> bool) -> Metaset.t -> bool
+
+module Metamap : Map.S with type key = metavariable
+
+val metamap_in_dom : metavariable -> 'a Metamap.t -> bool
+val metamap_to_list : 'a Metamap.t -> (metavariable * 'a) list
+val metamap_inv : 'a Metamap.t -> 'a -> metavariable list
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Metaset.t }
+
+val mk_freelisted : constr -> constr freelisted
+val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
+
+type clbinding =
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+val map_clb : (constr -> constr) -> clbinding -> clbinding
+
+type meta_map = clbinding Metamap.t
+val meta_defined : meta_map -> metavariable -> bool
+val meta_fvalue   : meta_map -> metavariable -> constr freelisted
+val meta_ftype    : meta_map -> metavariable -> constr freelisted
+val meta_declare : metavariable -> types -> meta_map -> meta_map
+val meta_assign  : metavariable -> constr -> meta_map -> meta_map