4 files changed, 12 insertions, 15 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 4bab801b1..8b5fe85e7 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 853135f10..538d8944d 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 c25a150f4..dc51c2384 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
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 35189f786..a0f565ce3 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -174,7 +174,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
 
 let dummy_goal env =
   let (gl,_,sigma) = 
-    Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in
+    Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
   {Evd.it = gl;
    Evd.sigma = sigma}