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

8 files changed, 53 insertions, 45 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6ed05d6b35..373a0bb62e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -972,7 +972,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> Errors.error "No focused goal."
   | g::_ ->
-    let gl = { Evd.it = g; sigma = glss.Evd.sigma; eff = Declareops.no_seff } in
+    let gl = { Evd.it = g; sigma = glss.Evd.sigma; } in
     pr_hint_term (pf_concl gl)
 
 (* displays the whole hint database db *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d80b7d738a..da6e123121 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -285,8 +285,8 @@ let make_autogoal_hints =
 	  unfreeze (Some (only_classes, sign, hints)); hints
 
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
-  { skft = fun sk fk {it = gl,hints; sigma=s;eff=eff} ->
-    let res = try Some (tac {it=gl; sigma=s;eff=eff})
+  { skft = fun sk fk {it = gl,hints; sigma=s;} ->
+    let res = try Some (tac {it=gl; sigma=s;})
               with e when catchable e -> None in
       match res with
       | Some gls -> sk (f gls hints) fk
@@ -294,7 +294,7 @@ let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : '
 
 let intro_tac : atac =
   lift_tactic Tactics.intro
-    (fun {it = gls; sigma = s;eff=eff} info ->
+    (fun {it = gls; sigma = s;} info ->
       let gls' =
 	List.map (fun g' ->
 	  let env = Goal.V82.env s g' in
@@ -303,13 +303,13 @@ let intro_tac : atac =
 	    (true,false,false) info.only_classes None (List.hd context) in
 	  let ldb = Hint_db.add_list hint info.hints in
 	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
-      in {it = gls'; sigma = s;eff=eff})
+      in {it = gls'; sigma = s;})
 
 let normevars_tac : atac =
-  { skft = fun sk fk {it = (gl, info); sigma = s; eff=eff} ->
+  { skft = fun sk fk {it = (gl, info); sigma = s;} ->
     let gl', sigma' = Goal.V82.nf_evar s gl in
     let info' = { info with auto_last_tac = lazy (str"normevars") } in
-      sk {it = [gl', info']; sigma = sigma';eff=eff} fk }
+      sk {it = [gl', info']; sigma = sigma';} fk }
 
 (* Ordering of states is lexicographic on the number of remaining goals. *)
 let compare (pri, _, _, res) (pri', _, _, res') =
@@ -324,9 +324,9 @@ let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
   { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
 
 let hints_tac hints =
-  { skft = fun sk fk {it = gl,info; sigma = s;eff=eff} ->
+  { skft = fun sk fk {it = gl,info; sigma = s;} ->
       let concl = Goal.V82.concl s gl in
-      let tacgl = {it = gl; sigma = s;eff=eff} in
+      let tacgl = {it = gl; sigma = s;} in
       let poss = e_possible_resolve hints info.hints concl in
       let rec aux i foundone = function
 	| (tac, _, b, name, pp) :: tl ->
@@ -338,7 +338,7 @@ let hints_tac hints =
 	  in
 	    (match res with
 	       | None -> aux i foundone tl
-	       | Some {it = gls; sigma = s';eff=eff} ->
+	       | Some {it = gls; sigma = s';} ->
 	    	   if !typeclasses_debug then
 		     msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
 			    ++ str" on" ++ spc () ++ pr_ev s gl);
@@ -370,11 +370,11 @@ let hints_tac hints =
 			      hints =
 			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
 			      then make_autogoal_hints info.only_classes
-				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';eff=eff}
+				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';}
 			      else info.hints;
 			      auto_cut = derivs }
 			in g, info) 1 newgls in
-		   let glsv = {it = gls'; sigma = s';eff=eff} in
+		   let glsv = {it = gls'; sigma = s';} in
 		     sk glsv fk)
 	| [] ->
 	  if not foundone && !typeclasses_debug then
@@ -417,14 +417,14 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 		       fk)
 		    else fk'
 		  in aux s' (gls'::acc) fk'' gls)
-	       fk {it = (gl,info); sigma = s; eff = Declareops.no_seff })
+	       fk {it = (gl,info); sigma = s; })
     | [] -> Somek2 (List.rev acc, s, fk)
-  in fun {it = gls; sigma = s; eff = eff} fk ->
+  in fun {it = gls; sigma = s; } fk ->
     let rec aux' = function
       | Nonek2 -> fk ()
       | Somek2 (res, s', fk') ->
 	  let goals' = List.concat res in
-	    sk {it = goals'; sigma = s'; eff = eff } (fun () -> aux' (fk' ()))
+	    sk {it = goals'; sigma = s'; } (fun () -> aux' (fk' ()))
     in aux' (aux s [] (fun () -> Nonek2) gls)
 
 let then_tac (first : atac) (second : atac) : atac =
@@ -463,8 +463,8 @@ let cut_of_hints h =
 let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
   let cut = cut_of_hints hints in
   { it = List.map_i (fun i g ->
-    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'; eff = Declareops.no_seff } in
-      (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; eff = Declareops.no_seff }
+    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'; } in
+      (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; }
 
 let get_result r =
   match r with
@@ -489,11 +489,11 @@ let eauto_tac ?limit hints =
   | Some limit -> fix_limit limit (eauto_tac hints)
 
 let eauto ?(only_classes=true) ?st ?limit hints g =
-  let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; eff=g.eff } in
+  let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; } in
     match run_tac (eauto_tac ?limit hints) gl with
     | None -> raise Not_found
-    | Some {it = goals; sigma = s; eff=eff} ->
-	{it = List.map fst goals; sigma = s; eff=eff}
+    | Some {it = goals; sigma = s; } ->
+	{it = List.map fst goals; sigma = s;}
 
 let real_eauto st ?limit hints p evd =
   let rec aux evd fails =
@@ -539,7 +539,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
   let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
-  let gls = { it = gl ; sigma = sigma; eff= Declareops.no_seff } in (* XXX eff *)
+  let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
   let gls' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
   let evd = sig_sig gls' in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1e01f47cd5..f5af80b0d5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -309,7 +309,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
   match kind_of_term hdcncl with
   | Ind ind -> 
       let c, eff = find_scheme scheme_name ind in 
-      let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
+      let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
       mkConst c, gl
   | _ -> assert false
 
@@ -809,7 +809,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl=
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = clenv_value_cast_meta absurd_clause in
-  let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
+  let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
   tclTHENS (cut_intro absurd_term)
     [onLastHypId gen_absurdity; refine pf] gl
 
@@ -1160,7 +1160,7 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl =
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
-    let gl = { gl with eff = Declareops.union_side_effects eff gl.eff } in
+    let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in
       (* cut with the good equality and prove the requested goal *)
     tclTHENS (cut (mkApp (ceq,new_eq_args)))
       [tclIDTAC; tclTHEN (apply (
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a935f69002..32affcbe75 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -115,8 +115,7 @@ TACTIC EXTEND ediscriminate
 END
 
 let discrHyp id gl =
-  discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
-              eff = gl.eff} gl
+  discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;} gl
 
 let injection_main c =
  elimOnConstrWithHoles (injClause None) false c
@@ -160,8 +159,7 @@ TACTIC EXTEND einjection_as
 END
 
 let injHyp id gl =
-  injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
-                   eff = gl.eff } gl
+  injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl; } gl
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 63a5917771..2a2a1e3560 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -242,8 +242,8 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 
 let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op =
   let pts = get_pftreestate() in
-  let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
-  let gl = { it = List.nth gls (n-1) ; sigma=sigma; eff=eff } in
+  let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
+  let gl = { it = List.nth gls (n-1) ; sigma=sigma; } in
   let t =
     try pf_get_hyp_typ gl id
     with Not_found -> Pretype_errors.error_var_not_found_loc loc id in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 7d3d5da612..fafafd8534 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1189,6 +1189,15 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
     | Some None -> Some None
     | None -> None
 
+(** ppedrot: this is a workaround. The current implementation of rewrite leaks
+    evar maps. We know that we should not produce effects in here, so we reput
+    them after computing... *)
+let tclEFFECT (tac : tactic) : tactic = fun gl ->
+  let eff = Evd.eval_side_effects gl.sigma in
+  let gls = tac gl in
+  let sigma = Evd.emit_side_effects eff (Evd.drop_side_effects gls.sigma) in
+  { gls with sigma; }
+
 let cl_rewrite_clause_tac ?abs strat clause gl =
   let evartac evd = Refiner.tclEVARS evd in
   let treat res =
@@ -1227,7 +1236,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
 	Refiner.tclFAIL 0
 	  (str"Unable to satisfy the rewriting constraints."
 	   ++ fnl () ++ Himsg.explain_typeclass_error env e)
-  in tac gl
+  in tclEFFECT tac gl
 
 
 let bind_gl_info f =
@@ -1266,8 +1275,7 @@ let assert_replacing id newt tac =
 		      in
 		      let (e, args) = destEvar ev in
 			Goal.return 
-                         (mkEvar (e, Array.of_list inst))
-                         Declareops.no_seff)))
+                         (mkEvar (e, Array.of_list inst)))))
        in Goal.bind reft Goal.refine)
   in Proofview.tclTHEN (Proofview.tclSENSITIVE sens) 
        (Proofview.tclFOCUS 2 2 tac)
@@ -1311,12 +1319,13 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	   try 
 	     let res = 
 	       cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp 
-	     in return (res, is_hyp) Declareops.no_seff
+	     in return (res, is_hyp)
 	   with
 	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	     raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
 			++ fnl () ++ Himsg.explain_typeclass_error env e)))
-  in Proofview.tclGOALBINDU info (fun i -> treat i)
+  in
+  Proofview.tclGOALBINDU info (fun i -> treat i)
   
 let newtactic_init_setoid () = 
   try init_setoid (); Proofview.tclUNIT ()
@@ -1726,10 +1735,10 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
     (), res
   in
     try
-      tclWEAK_PROGRESS 
+      (tclWEAK_PROGRESS 
 	(tclTHEN
            (Refiner.tclEVARS hypinfo.cl.evd)
-	   (cl_rewrite_clause_tac ~abs:hypinfo.abs strat cl)) gl
+	   (cl_rewrite_clause_tac ~abs:hypinfo.abs strat cl))) gl
     with RewriteFailure e ->
       let {l2r=l2r; c1=x; c2=y} = hypinfo in
 	raise (Pretype_errors.PretypeError
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 63d77af662..2a00f7defd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1045,7 +1045,7 @@ let mk_open_constr_value ist gl c =
 let mk_hyp_value ist gl c = Value.of_constr (mkVar (interp_hyp ist gl c))
 let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c)
 
-let pack_sigma eff (sigma,c) = {it=c;sigma=sigma;eff=eff}
+let pack_sigma (sigma,c) = {it=c;sigma=sigma;}
 
 let extend_gl_hyps { it=gl ; sigma=sigma } sign =
   Goal.V82.new_goal_with sigma gl sign
@@ -1316,7 +1316,7 @@ and interp_letin ist gl llc u =
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist goal lz lr lmr =
   let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in
-  let goal = { it = gl ; sigma = sigma; eff = sig_eff goal } in
+  let goal = { it = gl ; sigma = sigma; } in
   let hyps = pf_hyps goal in
   let hyps = if lr then List.rev hyps else hyps in
   let concl = pf_concl goal in
@@ -1456,11 +1456,11 @@ and interp_genarg ist gl x =
            (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
     | ConstrWithBindingsArgType ->
       in_gen (topwit wit_constr_with_bindings)
-        (pack_sigma (sig_eff gl) (interp_constr_with_bindings ist (pf_env gl) (project gl)
+        (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl)
 		       (out_gen (glbwit wit_constr_with_bindings) x)))
     | BindingsArgType ->
       in_gen (topwit wit_bindings)
-        (pack_sigma (sig_eff gl) (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
+        (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
     | ListArgType ConstrArgType ->
         let (sigma,v) = interp_genarg_constr_list ist gl x in
 	evdref := sigma;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 81ee6f19a0..298d26915f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3594,9 +3594,10 @@ let abstract_subproof id tac gl =
   (** ppedrot: seems legit to have abstracted subproofs as local*)
   let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
   let lem = mkConst cst in
-  let gl = {gl with eff =
-    Declareops.cons_side_effects
-      (Safe_typing.sideff_of_con (Global.safe_env()) cst) gl.eff} in
+  let open Declareops in
+  let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
+  let effs = cons_side_effects eff no_seff in
+  let gl = { gl with sigma = Evd.emit_side_effects effs gl.sigma; } in
   exact_no_check
     (applist (lem,List.rev (instance_from_named_context sign)))
     gl
@@ -3629,4 +3630,4 @@ let emit_side_effects eff gl =
   Declareops.iter_side_effects (fun e ->
     prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e))
     eff;
-  {gl with it = [gl.it] ; eff = Declareops.union_side_effects eff gl.eff}
+  { it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; }