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

28 files changed, 225 insertions, 221 deletions

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
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1aa8997710..84eba701ed 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -200,7 +200,8 @@ type evar_map = {
   univ_cstrs : Univ.universes;
   conv_pbs   : evar_constraint list;
   last_mods  : Evar.Set.t;
-  metas      : clbinding Metamap.t
+  metas      : clbinding Metamap.t;
+  effects    : Declareops.side_effects;
 }
 
 (*** Lifting primitive from EvarMap. ***)
@@ -361,6 +362,7 @@ let empty = {
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
+  effects    = Declareops.no_seff;
 }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
@@ -463,6 +465,17 @@ let collect_evars c =
   collrec Evar.Set.empty c
 
 (**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+  { evd with effects = Declareops.union_side_effects eff evd.effects; }
+
+let drop_side_effects evd =
+  { evd with effects = Declareops.no_seff; }
+
+let eval_side_effects evd = evd.effects
+
+(**********************************************************)
 (* Sort variables *)
 
 let new_univ_variable evd =
@@ -659,15 +672,11 @@ type open_constr = evar_map * constr
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  eff : Declareops.side_effects;
   sigma : evar_map
 }
 
 let sig_it x = x.it
-let sig_eff x = x.eff
 let sig_sig x = x.sigma
-let emit_side_effects eff x =
-  { x with eff = Declareops.union_side_effects eff x.eff }
 
 (**********************************************************)
 (* Failure explanation *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a5ff11c7ed..5ef243e136 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -195,6 +195,17 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
+(** {5 Side-effects} *)
+
+val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
+(** Push a side-effect into the evar map. *)
+
+val eval_side_effects : evar_map -> Declareops.side_effects
+(** Return the effects contained in the evar map. *)
+
+val drop_side_effects : evar_map -> evar_map
+(** This should not be used. For hacking purposes. *)
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
@@ -212,8 +223,6 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
 type 'a sigma = {
   it : 'a ;
   (** The base object. *)
-  eff : Declareops.side_effects;
-  (** Sideffects to be handled by the state machine. *)
   sigma : evar_map
   (** The added unification state. *)
 }
@@ -221,9 +230,7 @@ type 'a sigma = {
     ['a]. *)
 
 val sig_it  : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
 val sig_sig : 'a sigma -> evar_map
-val emit_side_effects : Declareops.side_effects -> 'a sigma -> 'a sigma
 
 (** {5 Meta machinery}
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 0e5d6721ed..2038fdeaa7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -388,7 +388,7 @@ let default_pr_subgoal n sigma =
     | [] -> error "No such goal."
     | g::rest ->
 	if Int.equal p 1 then
-          let pg = default_pr_goal { sigma=sigma ; it=g; eff=Declareops.no_seff } in
+          let pg = default_pr_goal { sigma=sigma ; it=g; } in
           v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
 	       ++ str " is:" ++ cut () ++ pg)
 	else
@@ -439,7 +439,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
   in
   let print_multiple_goals g l =
     if pr_first then
-      default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } ++
+      default_pr_goal { it = g ; sigma = sigma; } ++
       pr_rec 2 l
     else 
       pr_rec 1 (g::l)
@@ -464,13 +464,13 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
                  str "You can use Grab Existential Variables.")
       end
   | [g],[] when not !Flags.print_emacs ->
-      let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
+      let pg = default_pr_goal { it = g ; sigma = sigma; } in
       v 0 (
 	str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg
 	++ emacs_print_dependent_evars sigma seeds
       )
   | [g],a::l when not !Flags.print_emacs ->
-      let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
+      let pg = default_pr_goal { it = g ; sigma = sigma; } in
       v 0 (
 	str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg
 	++ emacs_print_dependent_evars sigma seeds
@@ -556,7 +556,7 @@ let pr_goal_by_id id =
 	 ++ pr_goal gs)
   in
   try
-    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;eff=Declareops.no_seff})
+    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;})
   with Not_found -> error "Invalid goal identifier."
 
 (* Elementary tactics *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 4260d5553b..a79c9f9785 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -113,7 +113,7 @@ let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
   let evd' = w_unify env evd CONV ~flags m n in
-  tclIDTAC {it = gls.it; sigma =  evd'; eff = gls.eff}
+  tclIDTAC {it = gls.it; sigma =  evd'; }
 
 let unify ?(flags=fail_quick_unif_flags) m gls =
   let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 68eb1c5861..0eacde8780 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -87,8 +87,7 @@ type subgoals = { subgoals: goal list }
    optimisation, since it will generaly not change during the
    evaluation. *)
 type 'a sensitive =
-    Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info ->
-      'a * Declareops.side_effects
+    Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a
 
 (* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
 (* the evar_info corresponding to the goal is computed at once
@@ -97,25 +96,24 @@ let eval t env defs gl =
   let info = content defs gl in
   let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
   let rdefs = ref defs in
-  let r, eff = t env rdefs gl info in
-  ( r , !rdefs, eff )
+  let r = t env rdefs gl info in
+  ( r , !rdefs )
 
 (* monadic bind on sensitive expressions *)
 let bind e f env rdefs goal info =
-  let a, eff1 = e env rdefs goal info in
-  let b, eff2 = f a env rdefs goal info in
-  b, Declareops.union_side_effects eff1 eff2
+  let a = e env rdefs goal info in
+  let b = f a env rdefs goal info in
+  b
 
 (* monadic return on sensitive expressions *)
-let return v e _ _ _ _ = v, e
+let return v _ _ _ _ = v
 
 (* interpretation of "open" constr *)
 (* spiwack: it is a wrapper around [Constrintern.interp_open_constr].
     In an ideal world, this could/should be the other way round.
     As of now, though, it seems at least quite useful to build tactics. *)
 let interp_constr cexpr env rdefs _ _ =
-  let c = Constrintern.interp_constr_evars rdefs env cexpr in
-  c, Declareops.no_seff
+  Constrintern.interp_constr_evars rdefs env cexpr
 
 (* Type of constr with holes used by refine. *)
 (* The list of evars doesn't necessarily contain all the evars in the constr,
@@ -135,18 +133,18 @@ module Refinable = struct
 
   let make t env rdefs gl info =
     let r = ref [] in
-    let me, eff = t r env rdefs gl info in
-    { me = me; my_evars = !r }, eff
+    let me = t r env rdefs gl info in
+    { me = me; my_evars = !r }
   let make_with t env rdefs gl info =
     let r = ref [] in
-    let (me,side), eff = t r env rdefs gl info in
-    ({ me = me ; my_evars = !r }, side), eff
+    let (me,side) = t r env rdefs gl info in
+    ({ me = me ; my_evars = !r }, side)
 
   let mkEvar handle env typ _ rdefs _ _ =
     let ev = Evarutil.e_new_evar rdefs env typ in
     let (e,_) = destEvar ev in
     handle := e::!handle;
-    ev, Declareops.no_seff
+    ev
 
   (* [with_type c typ] constrains term [c] to have type [typ].  *)
   let with_type t typ env rdefs _ _ =
@@ -160,14 +158,13 @@ module Refinable = struct
       Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ
     in
     rdefs := new_defs;
-    j'.Environ.uj_val, Declareops.no_seff
+    j'.Environ.uj_val
 
   (* spiwack: it is not very fine grain since it solves all typeclasses holes,
       not only those containing the current goal, or a given term. But it
       seems to fit our needs so far. *)
   let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ =
-    rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs;
-    (), Declareops.no_seff
+    rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs
 
 
 
@@ -228,13 +225,13 @@ module Refinable = struct
       Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc
     in
       ignore(update_handle handle init_defs !rdefs);
-      open_constr, Declareops.no_seff
+      open_constr
 
   let constr_of_open_constr handle check_type (evars, c) env rdefs gl info =
     let delta = update_handle handle !rdefs evars in
       rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
       if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
-      else c, Declareops.no_seff
+      else c
 
 end
 
@@ -255,7 +252,7 @@ let refine step env rdefs gl info =
   let subgoals =
     Option.List.flatten (List.map (advance !rdefs) subgoals)
   in
-  { subgoals = subgoals }, Declareops.no_seff
+  { subgoals = subgoals }
 
 
 (*** Cleaning  goals ***)
@@ -269,7 +266,7 @@ let clear ids env rdefs gl info =
   let (cleared_evar,_) = destEvar cleared_concl in
   let cleared_goal = descendent gl cleared_evar in
   rdefs := Evd.define gl.content cleared_concl !rdefs;
-  { subgoals = [cleared_goal] }, Declareops.no_seff
+  { subgoals = [cleared_goal] }
 
 let wrap_apply_to_hyp_and_dependent_on sign id f g =
   try Environ.apply_to_hyp_and_dependent_on sign id f g
@@ -325,27 +322,27 @@ let clear_body idents env rdefs gl info =
   let (new_evar,_) = destEvar new_constr in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_constr defs';
-  { subgoals = [new_goal] }, Declareops.no_seff
+  { subgoals = [new_goal] }
 
 
 (*** Sensitive primitives ***)
 
 (* [concl] is the conclusion of the current goal *)
 let concl _ _ _ info =
-  Evd.evar_concl info, Declareops.no_seff
+  Evd.evar_concl info
 
 (* [hyps] is the [named_context_val] representing the hypotheses
    of the current goal *)
 let hyps _ _ _ info =
-  Evd.evar_hyps info, Declareops.no_seff
+  Evd.evar_hyps info
 
 (* [env] is the current [Environ.env] containing both the
    environment in which the proof is ran, and the goal hypotheses *)
-let env env _ _ _ = env, Declareops.no_seff
+let env env _ _ _ = env
 
 (* [defs] is the [Evd.evar_map] at the current evaluation point *)
 let defs _ rdefs _ _ =
-  !rdefs, Declareops.no_seff
+  !rdefs
 
 (* Cf mli for more detailed comment.
     [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
@@ -363,7 +360,7 @@ let equal { content = e1 } { content = e2 } = Evar.equal e1 e2
 
 let here goal value _ _ goal' _ =
   if equal goal goal' then
-    value, Declareops.no_seff
+    value
   else
     raise UndefinedHere
 
@@ -375,7 +372,7 @@ let rec list_mem_with eq x = function
 
 let here_list goals value _ _ goal' _ =
   if list_mem_with equal goal' goals then
-    value, Declareops.no_seff
+    value
   else
     raise UndefinedHere
 
@@ -395,23 +392,23 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
        d)
   in
   (* Modified named context. *)
-  let new_hyps, effs1 =
-    let hyps, effs = hyps env rdefs gl info in
-    Environ.apply_to_hyp hyps id replace_function, effs
+  let new_hyps =
+    let hyps = hyps env rdefs gl info in
+    Environ.apply_to_hyp hyps id replace_function
   in
   let new_env = Environ.reset_with_named_context new_hyps env in
-  let new_constr, effs2 =
-    let concl, effs = concl env rdefs gl info in
-    Evarutil.e_new_evar rdefs new_env concl, effs
+  let new_constr =
+    let concl = concl env rdefs gl info in
+    Evarutil.e_new_evar rdefs new_env concl
   in
   let (new_evar,_) = destEvar new_constr in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_constr !rdefs;
-  { subgoals = [new_goal] }, Declareops.union_side_effects effs1 effs2
+  { subgoals = [new_goal] }
 
 let convert_concl check cl' env rdefs gl info =
   let sigma = !rdefs in
-  let cl, effs = concl env rdefs gl info in
+  let cl = concl env rdefs gl info in
   check_typability env sigma cl';
   if (not check) || Reductionops.is_conv_leq env sigma cl' cl then
     let new_constr =
@@ -420,7 +417,7 @@ let convert_concl check cl' env rdefs gl info =
     let (new_evar,_) = destEvar new_constr in
     let new_goal = descendent gl new_evar in
     rdefs := Evd.define gl.content new_constr !rdefs;
-    { subgoals = [new_goal] }, effs
+    { subgoals = [new_goal] }
   else
     Errors.error "convert-concl rule passed non-converting term"
 
@@ -433,20 +430,20 @@ let rename_hyp_sign id1 id2 sign =
     (fun (_,b,t) _ -> (id2,b,t))
     (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 let rename_hyp id1 id2 env rdefs gl info =
-  let hyps, effs1 = hyps env rdefs gl info in
+  let hyps = hyps env rdefs gl info in
   if not (Names.Id.equal id1 id2) &&
     List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
        Errors.error ((Names.Id.to_string id2)^" is already used.");
   let new_hyps = rename_hyp_sign id1 id2 hyps in
   let new_env = Environ.reset_with_named_context new_hyps env in
-  let old_concl, effs2 = concl env rdefs gl info in
+  let old_concl = concl env rdefs gl info in
   let new_concl = Vars.replace_vars [id1,mkVar id2] old_concl in
   let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
   let new_subproof = Vars.replace_vars [id2,mkVar id1] new_subproof in
   let (new_evar,_) = destEvar new_subproof in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_subproof !rdefs;
-  { subgoals = [new_goal] }, Declareops.union_side_effects effs1 effs2
+  { subgoals = [new_goal] }
 
 (*** Additional functions ***)
 
@@ -458,10 +455,10 @@ let rename_hyp id1 id2 env rdefs gl info =
 *)
 let rec list_map f l s =
   match l with
-  | [] -> ([],s,[])
-  | a::l -> let (a,s,e) = f s a in
-               let (l,s,es) = list_map f l s in
-	       (a::l,s,e::es)
+  | [] -> ([],s)
+  | a::l -> let (a,s) = f s a in
+               let (l,s) = list_map f l s in
+	       (a::l,s)
 
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture.
@@ -525,7 +522,7 @@ module V82 = struct
        to have functional content. *)
     let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
     let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty evi in
-    { Evd.it = build evk ; Evd.sigma = sigma; eff = Declareops.no_seff }
+    { Evd.it = build evk ; Evd.sigma = sigma; }
 
   (* Makes a goal out of an evar *)
   let build = build
@@ -567,7 +564,7 @@ module V82 = struct
       { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
     let new_evi = Typeclasses.mark_unresolvable new_evi in
     let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
-    { Evd.it = build evk ; sigma = new_sigma; eff = Declareops.no_seff }
+    { Evd.it = build evk ; sigma = new_sigma; }
 
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 267d264931..c07c7f28ed 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -43,13 +43,13 @@ type +'a sensitive
 (* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
 val eval :
   'a sensitive -> Environ.env -> Evd.evar_map -> goal ->
-    'a * Evd.evar_map * Declareops.side_effects
+    'a * Evd.evar_map
 
 (* monadic bind on sensitive expressions *)
 val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive
 
 (* monadic return on sensitive expressions *)
-val return : 'a -> Declareops.side_effects -> 'a sensitive
+val return : 'a -> 'a sensitive
 
 
 (* interpretation of "open" constr *)
@@ -171,9 +171,9 @@ val here_list : goal list -> 'a -> 'a sensitive
    [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
    new evar_map to next definition *)
 val list_map : 
-  (Evd.evar_map -> 'a -> 'b * Evd.evar_map * Declareops.side_effects) ->
+  (Evd.evar_map -> 'a -> 'b * Evd.evar_map) ->
   'a list -> Evd.evar_map ->
-    'b list * Evd.evar_map * Declareops.side_effects list
+    'b list * Evd.evar_map
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e93319cae8..f883317503 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -573,10 +573,10 @@ let prim_refiner r sigma goal =
 	      Goal.list_map (fun sigma (_,_,c) ->
                 let gl,ev,sig' =
                   Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sig',Declareops.no_seff)
+                (gl,ev),sig')
               all sigma
 	in
-	let (gls_evs,sigma,_) =  mk_sign sign all in
+	let (gls_evs,sigma) =  mk_sign sign all in
 	let (gls,evs) = List.split gls_evs in
 	let ids = List.map pi1 all in
 	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
@@ -615,10 +615,10 @@ let prim_refiner r sigma goal =
               Goal.list_map (fun sigma(_,c) ->
                 let gl,ev,sigma =
                   Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sigma,Declareops.no_seff)
-              all sigma                                      
+                (gl,ev),sigma)
+              all sigma
      	in
-	let (gls_evs,sigma,_) =  mk_sign sign all in
+	let (gls_evs,sigma) =  mk_sign sign all in
 	let (gls,evs) = List.split gls_evs in
 	let (ids,types) = List.split all in
 	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a45fe179ae..a44b3bef3a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -62,15 +62,15 @@ let _ = Errors.register_handler begin function
 end
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
-  let { it=goals ; sigma = sigma; eff = eff } = Proof.V82.subgoals p in
+  let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
   try
-          { it=(List.nth goals (i-1)) ; sigma=sigma; eff = eff }
+          { it=(List.nth goals (i-1)) ; sigma=sigma; }
   with Failure _ -> raise NoSuchGoal
     
 let get_goal_context_gen i =
   try
-let { it=goal ; sigma=sigma; eff=eff } =  get_nth_V82_goal i in
-(sigma, Refiner.pf_env { it=goal ; sigma=sigma; eff=eff })
+let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
+(sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
   with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
 
 let get_goal_context i =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8ad2458afa..712845f584 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -234,7 +234,7 @@ let _ = Errors.register_handler begin function
   | _ -> raise Errors.Unhandled
 end
 
-let return p t =
+let return p =
   if not (is_done p) then
     raise UnfinishedProof
   else if has_unresolved_evar p then
@@ -242,7 +242,7 @@ let return p t =
     raise HasUnresolvedEvar
   else
     let p = unfocus end_of_stack_kind p () in
-    Proofview.return p.proofview t
+    Proofview.return p.proofview
 
 let initial_goals p = Proofview.initial_goals p.proofview
 
@@ -271,10 +271,10 @@ module V82 = struct
     Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
 
   let top_goal p =
-    let { Evd.it=gls ; sigma=sigma; eff=eff } =
+    let { Evd.it=gls ; sigma=sigma; } =
 	Proofview.V82.top_goals p.proofview
     in
-    { Evd.it=List.hd gls ; sigma=sigma; eff=eff }
+    { Evd.it=List.hd gls ; sigma=sigma; }
 
   let top_evars p =
     Proofview.V82.top_evars p.proofview
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 70615e09e3..fa6007061b 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -61,8 +61,7 @@ val partial_proof : proof -> Term.constr list
     Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
 exception UnfinishedProof
 exception HasUnresolvedEvar
-val return :
-  proof -> Term.constr -> Term.constr * Declareops.side_effects
+val return : proof -> Evd.evar_map
 
 (*** Focusing actions ***)
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d773eeb43d..81bfcaccee 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -280,16 +280,21 @@ let close_proof ~now fpl =
 let return_proof ~fix_exn =
   let { proof } = cur_pstate () in
   let initial_goals = Proof.initial_goals proof in
-  List.map (fun (c, _) ->
-   try Proof.return proof c with
+  let evd =
+   try Proof.return proof with
    | Proof.UnfinishedProof ->
        raise (fix_exn(Errors.UserError("last tactic before Qed",
          str"Attempt to save an incomplete proof")))
    | Proof.HasUnresolvedEvar ->
        raise (fix_exn(Errors.UserError("last tactic before Qed",
          str"Attempt to save a proof with existential " ++
-         str"variables still non-instantiated"))))
-   initial_goals
+         str"variables still non-instantiated")))
+  in
+  let eff = Evd.eval_side_effects evd in
+  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+      side-effects... This may explain why one need to uniquize side-effects
+      thereafter... *)
+  List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals
 
 let close_future_proof proof = close_proof ~now:false proof
 let close_proof () =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9467d2d710..625ae74f12 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -27,7 +27,6 @@ type proofview = {
      initial : (Term.constr * Term.types) list;
      solution : Evd.evar_map;
      comb : Goal.goal list;
-     side_effects : Declareops.side_effects
      }
 
 let proofview p =
@@ -40,7 +39,6 @@ let init =
   | [] ->  { initial = [] ; 
 	     solution = Evd.empty ;
              comb = [];
-             side_effects = Declareops.no_seff
 	   }
   | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
                            aux l
@@ -52,8 +50,7 @@ let init =
 			 let gl = Goal.build e in
 			 { initial = (econstr,typ)::ret;
 			   solution = new_defs ;
-                           comb = gl::comb;
-                           side_effects = Declareops.no_seff }
+                           comb = gl::comb; }
   in
   fun l -> let v = aux l in
     (* Marks all the goal unresolvable for typeclasses. *)
@@ -69,13 +66,15 @@ let finished = function
   | _  -> false
 
 (* Returns the current value of the proofview partial proofs. *)
-let return { solution=defs; side_effects=eff } c = Evarutil.nf_evar defs c, eff
+let return { solution=defs } = defs
+
+let return_constr { solution = defs } c = Evarutil.nf_evar defs c
 
 let partial_proof pv =
-  List.map fst (List.map (return pv) (List.map fst (initial_goals pv)))
+  List.map (return_constr pv) (List.map fst (initial_goals pv))
 
 let emit_side_effects eff x =
-  { x with side_effects = Declareops.union_side_effects eff x.side_effects }
+  { x with solution = Evd.emit_side_effects eff x.solution }
 
 (* spiwack: this function should probably go in the Util section,
     but I'd rather have Util (or a separate module for lists)
@@ -366,8 +365,8 @@ let rec catchable_exception = function
    [s] to each goal successively and applying [k] to each result. *)
 let list_of_sensitive s k env step =
   Goal.list_map begin fun defs g ->
-    let (a,defs,effs) = Goal.eval s env defs g in
-    (k a) , defs, effs
+    let (a,defs) = Goal.eval s env defs g in
+    (k a) , defs
   end step.comb step.solution
 (* In form of a tactic *)
 let list_of_sensitive s k env =
@@ -376,10 +375,8 @@ let list_of_sensitive s k env =
   let (>>) = Inner.seq in
   Inner.get >>= fun step ->
   try 
-    let (tacs,defs,effs) = list_of_sensitive s k env step in
-    Inner.set { step with solution = defs;
-      side_effects = Declareops.union_side_effects step.side_effects 
-        (Declareops.flatten_side_effects effs) } >>
+    let (tacs,defs) = list_of_sensitive s k env step in
+    Inner.set { step with solution = defs; } >>
     Inner.return tacs
   with e when catchable_exception e ->
     tclZERO e env
@@ -400,23 +397,20 @@ let tclGOALBINDU s k =
 (* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
     everything is done in one step. *)
 let sensitive_on_proofview s env step =
-  let wrap g ((defs, partial_list, partial_eff) as partial_res) = 
+  let wrap g ((defs, partial_list) as partial_res) = 
     match Goal.advance defs g with
     | None -> partial_res
     | Some g ->
-      let { Goal.subgoals = sg } , d', eff = Goal.eval s env defs g in
-      (d', sg::partial_list, eff::partial_eff)
+      let { Goal.subgoals = sg } , d' = Goal.eval s env defs g in
+      (d', sg::partial_list)
   in
-  let ( new_defs , combed_subgoals, side_effects ) = 
-    List.fold_right wrap step.comb (step.solution,[],[])
+  let ( new_defs , combed_subgoals ) = 
+    List.fold_right wrap step.comb (step.solution,[])
   in
   { step with
      solution = new_defs;
-     comb = List.flatten combed_subgoals;
-     side_effects =
-       Declareops.union_side_effects
-         (Declareops.flatten_side_effects side_effects) step.side_effects }
-let tclSENSITIVE s env =
+     comb = List.flatten combed_subgoals; }
+  let tclSENSITIVE s env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Inner.bind in
   Inner.get >>= fun step ->
@@ -456,25 +450,18 @@ module V82 = struct
     try
       let tac evd gl = 
         let glsigma  =
-          tac { Evd.it = gl ; sigma = evd; eff = Declareops.no_seff }  in
+          tac { Evd.it = gl ; sigma = evd; }  in
         let sigma = glsigma.Evd.sigma in
         let g = glsigma.Evd.it in
-        ( g, sigma, glsigma.Evd.eff )
+        ( g, sigma )
       in
     (* Old style tactics expect the goals normalized with respect to evars. *)
-      let no_side_eff f x y =
-        let a, b = f x y in a, b, Declareops.no_seff in
-      let (initgoals,initevd, eff1) = 
-        Goal.list_map (no_side_eff Goal.V82.nf_evar) ps.comb ps.solution
+      let (initgoals,initevd) =
+        Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
       in
-      let (goalss,evd,eff2) = Goal.list_map tac initgoals initevd in
+      let (goalss,evd) = Goal.list_map tac initgoals initevd in
       let sgs = List.flatten goalss in
-      Inner.set { ps with solution=evd ; comb=sgs; 
-        side_effects =
-          Declareops.union_side_effects ps.side_effects 
-            (Declareops.union_side_effects 
-              (Declareops.flatten_side_effects eff1)
-              (Declareops.flatten_side_effects eff2)) }
+      Inner.set { ps with solution=evd ; comb=sgs; }
     with e when catchable_exception e ->
       tclZERO e env
 
@@ -495,12 +482,12 @@ module V82 = struct
 
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
-  let goals { comb = comb ; solution = solution; side_effects=eff } =
-   { Evd.it = comb ; sigma = solution; eff=eff}
+  let goals { comb = comb ; solution = solution; } =
+   { Evd.it = comb ; sigma = solution }
 
-  let top_goals { initial=initial ; solution=solution; side_effects=eff } =
+  let top_goals { initial=initial ; solution=solution; } =
     let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
-    { Evd.it = goals ; sigma=solution; eff=eff }
+    { Evd.it = goals ; sigma=solution; }
 
   let top_evars { initial=initial } =
     let evars_of_initial (c,_) =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 2869e75e10..135b7205f2 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -44,7 +44,7 @@ val init : (Environ.env * Term.types) list -> proofview
 val finished : proofview -> bool
 
 (* Returns the current value of the proofview partial proofs. *)
-val return : proofview -> constr -> constr * Declareops.side_effects
+val return : proofview -> Evd.evar_map
 
 val partial_proof : proofview -> constr list
 val initial_goals : proofview -> (constr * types) list
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 06e35284d4..66e251d55c 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -16,7 +16,6 @@ open Logic
 
 
 let sig_it x = x.it
-let sig_eff x = x.eff
 let project x = x.sigma
 
 (* Getting env *)
@@ -26,7 +25,7 @@ let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)
 
 let refiner pr goal_sigma =
   let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
-  { it = sgl; sigma = sigma'; eff = goal_sigma.eff }
+  { it = sgl; sigma = sigma'; }
 
 let norm_evar_tac gl = refiner (Change_evars) gl
 
@@ -35,19 +34,18 @@ let norm_evar_tac gl = refiner (Change_evars) gl
 (*********************)
 
 
-let unpackage glsig = (ref (glsig.sigma)), glsig.it, (ref (glsig.eff))
+let unpackage glsig = (ref (glsig.sigma)), glsig.it
 
-let repackage e r v = {it = v; sigma = !r; eff = !e}
+let repackage r v = {it = v; sigma = !r; }
 
-let apply_sig_tac eff r tac g =
+let apply_sig_tac r tac g =
   check_for_interrupt (); (* Breakpoint *)
-  let glsigma = tac (repackage eff r g) in
+  let glsigma = tac (repackage r g) in
   r := glsigma.sigma;
-  eff := glsigma.eff;
   glsigma.it
 
 (* [goal_goal_list : goal sigma -> goal list sigma] *)
-let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; eff=gls.eff}
+let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; }
 
 (* forces propagation of evar constraints *)
 let tclNORMEVAR = norm_evar_tac
@@ -71,32 +69,32 @@ let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
 let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
 
 let start_tac gls =
-  let sigr, g, eff = unpackage gls in
-  (sigr, [g], eff)
+  let sigr, g = unpackage gls in
+  (sigr, [g])
 
-let finish_tac (sigr,gl,eff) = repackage eff sigr gl
+let finish_tac (sigr,gl) = repackage sigr gl
 
 (* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last
    m subgoals, and [tac] on the others *)
-let thens3parts_tac tacfi tac tacli (sigr,gs,eff) =
+let thens3parts_tac tacfi tac tacli (sigr,gs) =
   let nf = Array.length tacfi in
   let nl = Array.length tacli in
   let ng = List.length gs in
   if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll =
       (List.map_i (fun i ->
-        apply_sig_tac eff sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
+        apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
 	0 gs) in
-    (sigr,List.flatten gll, eff)
+    (sigr,List.flatten gll)
 
 (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
 let thensf_tac taci tac = thens3parts_tac taci tac [||]
 
 (* Apply [tac i] on the ith subgoal (no subgoals number check) *)
-let thensi_tac tac (sigr,gs,eff) =
+let thensi_tac tac (sigr,gs) =
   let gll =
-    List.map_i (fun i -> apply_sig_tac eff sigr (tac i)) 1 gs in
-  (sigr, List.flatten gll, eff)
+    List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
+  (sigr, List.flatten gll)
 
 let then_tac tac = thensf_tac [||] tac
 
@@ -198,9 +196,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
   let oldhyps:Context.named_context = pf_hyps goal in
   let rslt:Proof_type.goal list Evd.sigma = tac goal in
-  let {it=gls;sigma=sigma;eff=eff} = rslt in
+  let { it = gls; sigma = sigma; } = rslt in
   let hyps:Context.named_context list =
-    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; eff=eff}) gls in
+    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
   let newhyps =
     List.map (fun hypl -> List.subtract hypl oldhyps) hyps in
   let emacs_str s =
@@ -250,8 +248,8 @@ let tclORELSE_THEN t1 t2then t2else gls =
   with
     | None -> t2else gls
     | Some sgl ->
-        let sigr, gl, eff = unpackage sgl in
-        finish_tac (then_tac t2then  (sigr,gl,eff))
+        let sigr, gl = unpackage sgl in
+        finish_tac (then_tac t2then  (sigr,gl))
 
 (* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
 let tclTRY f = (tclORELSE0 f tclIDTAC)
@@ -356,24 +354,24 @@ let tclIDTAC_list gls = gls
 (* first_goal : goal list sigma -> goal sigma *)
 
 let first_goal gls =
-  let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in
+  let gl = gls.it and sig_0 = gls.sigma in
   if List.is_empty gl then error "first_goal";
-  { it = List.hd gl; sigma = sig_0 ; eff = eff_0 }
+  { it = List.hd gl; sigma = sig_0; }
 
 (* goal_goal_list : goal sigma -> goal list sigma *)
 
 let goal_goal_list gls =
-  let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in 
-  { it = [gl]; sigma = sig_0; eff = eff_0 }
+  let gl = gls.it and sig_0 = gls.sigma in 
+  { it = [gl]; sigma = sig_0; }
 
 (* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
 
 let apply_tac_list tac glls =
-  let (sigr,lg,eff) = unpackage glls in
+  let (sigr,lg) = unpackage glls in
   match lg with
   | (g1::rest) ->
-      let gl = apply_sig_tac eff sigr tac g1 in
-      repackage eff sigr (gl@rest)
+      let gl = apply_sig_tac sigr tac g1 in
+      repackage sigr (gl@rest)
   | _ -> error "apply_tac_list"
 
 let then_tactic_list tacl1 tacl2 glls =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index b2e753ea33..c198958e3d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -16,17 +16,15 @@ open Logic
 (** The refiner (handles primitive rules and high-level tactics). *)
 
 val sig_it  : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
 val project : 'a sigma -> evar_map
 
 val pf_env  : goal sigma -> Environ.env
 val pf_hyps : goal sigma -> named_context
 
-val unpackage : 'a sigma -> evar_map ref * 'a * Declareops.side_effects ref
-val repackage : Declareops.side_effects ref -> evar_map ref -> 'a -> 'a sigma
+val unpackage : 'a sigma -> evar_map ref * 'a
+val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
-  Declareops.side_effects ref -> evar_map ref -> 
-    (goal sigma -> goal list sigma) -> goal -> goal list
+  evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
 
 val refiner : rule -> tactic
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fad46c99ba..84553e9ebc 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -22,7 +22,7 @@ open Proof_type
 open Logic
 open Refiner
 
-let re_sig it eff  gc = { it = it; sigma = gc; eff = eff }
+let re_sig it  gc = { it = it; sigma = gc; }
 
 (**************************************************************)
 (* Operations for handling terms under a local typing context *)
@@ -36,7 +36,6 @@ let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
 
 let sig_it   = Refiner.sig_it
-let sig_eff  = Refiner.sig_eff
 let project  = Refiner.project
 let pf_env   = Refiner.pf_env
 let pf_hyps  = Refiner.pf_hyps
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 19eb9ba7c0..ab59c64416 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -27,16 +27,14 @@ type 'a sigma   = 'a Evd.sigma;;
 type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a
-val sig_eff : 'a sigma   -> Declareops.side_effects
 val project : goal sigma -> evar_map
 
-val re_sig : 'a -> Declareops.side_effects -> evar_map -> 'a sigma
+val re_sig : 'a -> evar_map -> 'a sigma
 
-val unpackage : 'a sigma -> evar_map ref * 'a * Declareops.side_effects ref
-val repackage : Declareops.side_effects ref -> evar_map ref -> 'a -> 'a sigma
+val unpackage : 'a sigma -> evar_map ref * 'a
+val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
-  Declareops.side_effects ref -> evar_map ref -> 
-  (goal sigma -> (goal list) sigma) -> goal -> (goal list) 
+  evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
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; }
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cd248e4cc3..8abac272c0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -93,8 +93,8 @@ let try_print_subgoals () =
 
 let show_intro all =
   let pf = get_pftreestate() in
-  let {Evd.it=gls ; sigma=sigma; eff=eff} = Proof.V82.subgoals pf in
-  let gl = {Evd.it=List.hd gls ; sigma = sigma; eff=eff} in
+  let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+  let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
   let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
   if all
   then