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

14 files changed, 134 insertions, 153 deletions

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