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

3 files changed, 11 insertions, 14 deletions

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 4bab801b1c..8b5fe85e76 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -20,8 +20,6 @@ let get_daimon_flag () = !daimon_flag
 
 
 
-(* Information associated to goals. *)
-open Store.Field
 
 type split_tree=
     Skip_patt of Id.Set.t * split_tree
@@ -69,10 +67,9 @@ let mode_of_pftreestate pts =
   (* spiwack: it used to be "top_goal_..." but this should be fine *)
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let goal = List.hd goals in
-    if info.get (Goal.V82.extra sigma goal) = None then
-      Mode_tactic 
-    else
-      Mode_proof
+  match Store.get (Goal.V82.extra sigma goal) info with
+  | None -> Mode_tactic 
+  | Some _ -> Mode_proof
 	  
 let get_current_mode () =
   try 
@@ -84,12 +81,12 @@ let check_not_proof_mode str =
    error str
 
 let get_info sigma gl=
-  match info.get (Goal.V82.extra sigma gl) with
+  match Store.get (Goal.V82.extra sigma gl) info with
   | None ->  invalid_arg "get_info"
   | Some pm -> pm
 
 let try_get_info sigma gl =
-  info.get (Goal.V82.extra sigma gl)
+  Store.get (Goal.V82.extra sigma gl) info
 
 let get_stack pts =
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 853135f101..538d8944d7 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -59,7 +59,7 @@ type stack_info =
 type pm_info =
     {pm_stack : stack_info list }
 
-val info : pm_info Store.Field.t
+val info : pm_info Store.field
 
 val get_info : Evd.evar_map -> Proof_type.goal -> pm_info
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c25a150f4e..dc51c23849 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -57,13 +57,13 @@ let tcl_change_info_gen info_gen =
      let sigma = Goal.V82.partial_solution sigma (sig_it gls) ev in
      { it = [gl] ; sigma= sigma } )
 
-open Store.Field
-
-let tcl_change_info info gls =  
-  let info_gen = Decl_mode.info.set info in
+let tcl_change_info info gls =
+  let info_gen s = Store.set s Decl_mode.info info in
   tcl_change_info_gen info_gen gls
 
-let tcl_erase_info gls =  tcl_change_info_gen (Decl_mode.info.remove) gls
+let tcl_erase_info gls =
+  let info_gen s = Store.remove s Decl_mode.info in
+  tcl_change_info_gen info_gen gls
 
 let special_whd gl=
   let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in