From 65eec025bc0b581fae1af78f18d1a8666b76e69b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 5 Oct 2013 17:44:45 +0000
Subject: Moving side effects into evar_map. There was no reason to keep
 another state out of one we were threading all the way along. This should be
 safer, as one cannot forego side effects accidentally by manipulating
 explicitly the [sigma] container.

Still, this patch raised the issue of badly used evar maps. There
is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the
fact it uses evar maps in an unorthodox way.

Likewise, that mean we have to revert all contrib patches that added
effect threading...

There was also a dubious use of side effects in their toplevel handling,
that duplicates them, leading to the need of a rather unsafe List.uniquize
afterwards. It should be investigaged.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/decl_proof_instr.ml | 10 +++++-----
 plugins/setoid_ring/newring.ml4       |  3 +--
 2 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index cca17a17e1..e18df6e460 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -51,13 +51,13 @@ let _ =
 
 let tcl_change_info_gen info_gen =
   (fun gls ->
-     let it, eff = sig_it gls, sig_eff gls in
+     let it = sig_it gls in
      let concl = pf_concl gls in
      let hyps = Goal.V82.hyps (project gls) it in
      let extra = Goal.V82.extra (project gls) it in
      let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
      let sigma = Goal.V82.partial_solution sigma it ev in
-     { it = [gl] ; sigma= sigma; eff = eff } )
+     { it = [gl] ; sigma= sigma; } )
 
 let tcl_change_info info gls =
   let info_gen s = Store.set s Decl_mode.info info in
@@ -129,7 +129,7 @@ let go_to_proof_mode () =
 
 let daimon_tac gls =
   set_daimon_flag ();
-  {it=[];sigma=sig_sig gls;eff=gls.eff}
+  {it=[];sigma=sig_sig gls;}
 
 (* post-instruction focus management *)
 
@@ -1455,8 +1455,8 @@ let do_instr raw_instr pts =
   let has_tactic = preprocess pts raw_instr.instr in
   begin
     if has_tactic then
-            let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
-      let gl = { it=List.hd gls ; sigma=sigma; eff=eff } in
+            let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
+      let gl = { it=List.hd gls ; sigma=sigma; } in
       let env=  pf_env gl in
       let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
 		 gsigma = sigma; genv = env} in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 30ceb10182..74ad34eff6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -179,8 +179,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 Evd.Store.empty in
-  {Evd.it = gl; Evd.eff=Declareops.no_seff;
-   Evd.sigma = sigma}
+  {Evd.it = gl; Evd.sigma = sigma}
 
 let exec_tactic env n f args =
   let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
-- 
cgit v1.2.3