Allowing different types of, not to be mixed, generic Stores through

functor application. Rewritten the interface btw.

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

5 files changed, 9 insertions, 7 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 39d6a59db6..d9a22b3e78 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -378,8 +378,6 @@ type clear_dependency_error =
 
 exception ClearDependencyError of Id.t * clear_dependency_error
 
-open Store.Field
-
 let cleared = Store.field ()
 
 let rec check_and_clear_in_constr evdref err ids c =
@@ -448,7 +446,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
 	      let evi = Evd.find !evdref evk in
 	      let extra = evi.evar_extra in
-	      let extra' = cleared.set true extra in
+	      let extra' = Store.set extra cleared true in
 	      let evi' = { evi with evar_extra = extra' } in
 	      evdref := Evd.add !evdref evk evi' ;
 	    (* spiwack: /hacking session *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7f605ce3a2..92e8193813 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -186,7 +186,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error
 
 (* spiwack: marks an evar that has been "defined" by clear.
     used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
-val cleared : bool Store.Field.t
+val cleared : bool Store.field
 
 val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
   Id.t list -> named_context_val * types
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index f9ca6a2415..0f709e454f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -21,6 +21,9 @@ open Mod_subst
 
 (* The type of mappings for existential variables *)
 
+module Dummy = struct end
+module Store = Store.Make(Dummy)
+
 type evar = Term.existential_key
 
 let string_of_existential evk = "?" ^ string_of_int evk
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index b3866e3209..f7ec791b7c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -95,6 +95,8 @@ type evar_body =
   | Evar_empty
   | Evar_defined of constr
 
+module Store : Store.S
+
 type evar_info = {
   evar_concl : constr;
   evar_hyps : named_context_val;
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 0fe13ef9ca..c477013d88 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -485,14 +485,13 @@ let is_implicit_arg = function
  *)
 
 let resolvable = Store.field ()
-open Store.Field
 
 let is_resolvable evi =
   assert (match evi.evar_body with Evar_empty -> true | _ -> false);
-  Option.default true (resolvable.get evi.evar_extra)
+  Option.default true (Store.get evi.evar_extra resolvable)
 
 let mark_resolvability_undef b evi =
-  let t = resolvable.set b evi.evar_extra in
+  let t = Store.set evi.evar_extra resolvable b in
   { evi with evar_extra = t }
 
 let mark_resolvability b evi =