State Transaction Machine

The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).

The observe id function runs the transactions necessary to reach to the
state id.  Transaction being on a merged branch are not executed but
stored into a future.

The finish function calls observe on the tip of the current branch.

Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.

This is the work described in the Coq Workshop 2012 paper.

Coq is compile with thread support from now on.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 446 insertions, 617 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 389075c9a..7b1ccd542 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'}
+  tclIDTAC {it = gls.it; sigma =  evd'; eff = gls.eff}
 
 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 67cd41412..c6e2c2ed9 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -87,7 +87,8 @@ 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
+    Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info ->
+      'a * Declareops.side_effects
 
 (* 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
@@ -96,22 +97,25 @@ 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 = t env rdefs gl info in
-  ( r , !rdefs )
+  let r, eff = t env rdefs gl info in
+  ( r , !rdefs, eff )
 
 (* monadic bind on sensitive expressions *)
 let bind e f env rdefs goal info =
-  f (e env rdefs goal info) 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
 
 (* monadic return on sensitive expressions *)
-let return v _ _ _ _ = v
+let return v e _ _ _ _ = v, e
 
 (* 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 _ _ =
-  Constrintern.interp_constr_evars rdefs env cexpr
+  let c = Constrintern.interp_constr_evars rdefs env cexpr in
+  c, Declareops.no_seff
 
 (* Type of constr with holes used by refine. *)
 (* The list of evars doesn't necessarily contain all the evars in the constr,
@@ -131,19 +135,18 @@ module Refinable = struct
 
   let make t env rdefs gl info =
     let r = ref [] in
-    let me = t r env rdefs gl info in
-    { me = me;
-       my_evars = !r }
+    let me, eff = t r env rdefs gl info in
+    { me = me; my_evars = !r }, eff
   let make_with t env rdefs gl info =
     let r = ref [] in
-    let (me,side) = t r env rdefs gl info in
-    { me = me ; my_evars = !r } , side
+    let (me,side), eff = t r env rdefs gl info in
+    ({ me = me ; my_evars = !r }, side), eff
 
   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
+    ev, Declareops.no_seff
 
   (* [with_type c typ] constrains term [c] to have type [typ].  *)
   let with_type t typ env rdefs _ _ =
@@ -157,14 +160,14 @@ module Refinable = struct
       Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ
     in
     rdefs := new_defs;
-    j'.Environ.uj_val
+    j'.Environ.uj_val, Declareops.no_seff
 
   (* 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
 
 
 
@@ -225,13 +228,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
+      open_constr, Declareops.no_seff
 
   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
+      else c, Declareops.no_seff
 
 end
 
@@ -252,7 +255,7 @@ let refine step env rdefs gl info =
   let subgoals =
     Option.List.flatten (List.map (advance !rdefs) subgoals)
   in
-  { subgoals = subgoals }
+  { subgoals = subgoals }, Declareops.no_seff
 
 
 (*** Cleaning  goals ***)
@@ -266,7 +269,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] }
+  { subgoals = [cleared_goal] }, Declareops.no_seff
 
 let wrap_apply_to_hyp_and_dependent_on sign id f g =
   try Environ.apply_to_hyp_and_dependent_on sign id f g
@@ -322,27 +325,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] }
+  { subgoals = [new_goal] }, Declareops.no_seff
 
 
 (*** Sensitive primitives ***)
 
 (* [concl] is the conclusion of the current goal *)
 let concl _ _ _ info =
-  Evd.evar_concl info
+  Evd.evar_concl info, Declareops.no_seff
 
 (* [hyps] is the [named_context_val] representing the hypotheses
    of the current goal *)
 let hyps _ _ _ info =
-  Evd.evar_hyps info
+  Evd.evar_hyps info, Declareops.no_seff
 
 (* [env] is the current [Environ.env] containing both the
    environment in which the proof is ran, and the goal hypotheses *)
-let env env _ _ _ = env
+let env env _ _ _ = env, Declareops.no_seff
 
 (* [defs] is the [Evd.evar_map] at the current evaluation point *)
 let defs _ rdefs _ _ =
-  !rdefs
+  !rdefs, Declareops.no_seff
 
 (* Cf mli for more detailed comment.
     [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
@@ -360,7 +363,7 @@ let equal { content = e1 } { content = e2 } = Int.equal e1 e2
 
 let here goal value _ _ goal' _ =
   if equal goal goal' then
-    value
+    value, Declareops.no_seff
   else
     raise UndefinedHere
 
@@ -372,7 +375,7 @@ let rec list_mem_with eq x = function
 
 let here_list goals value _ _ goal' _ =
   if list_mem_with equal goal' goals then
-    value
+    value, Declareops.no_seff
   else
     raise UndefinedHere
 
@@ -392,21 +395,23 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
        d)
   in
   (* Modified named context. *)
-  let new_hyps =
-    Environ.apply_to_hyp (hyps env rdefs gl info) id replace_function
+  let new_hyps, effs1 =
+    let hyps, effs = hyps env rdefs gl info in
+    Environ.apply_to_hyp hyps id replace_function, effs
   in
   let new_env = Environ.reset_with_named_context new_hyps env in
-  let new_constr =
-    Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
+  let new_constr, effs2 =
+    let concl, effs = concl env rdefs gl info in
+    Evarutil.e_new_evar rdefs new_env concl, effs
   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] }
+  { subgoals = [new_goal] }, Declareops.union_side_effects effs1 effs2
 
 let convert_concl check cl' env rdefs gl info =
   let sigma = !rdefs in
-  let cl = concl env rdefs gl info in
+  let cl, effs = 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 =
@@ -415,7 +420,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] }
+    { subgoals = [new_goal] }, effs
   else
     Errors.error "convert-concl rule passed non-converting term"
 
@@ -428,19 +433,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 = hyps env rdefs gl info in
+  let hyps, effs1 = 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 new_concl = Vars.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
+  let old_concl, effs2 = 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] }
+  { subgoals = [new_goal] }, Declareops.union_side_effects effs1 effs2
 
 (*** Additional functions ***)
 
@@ -452,10 +458,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) = f s a in
-               let (l,s) = list_map f l s in
-	       (a::l,s)
+  | [] -> ([],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)
 
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture.
@@ -521,7 +527,7 @@ module V82 = struct
     let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
     let evk = Evarutil.new_untyped_evar () in
     let sigma = Evd.add Evd.empty evk evi in
-    { Evd.it = build evk ; Evd.sigma = sigma }
+    { Evd.it = build evk ; Evd.sigma = sigma; eff = Declareops.no_seff }
 
   (* Makes a goal out of an evar *)
   let build = build
@@ -564,7 +570,7 @@ module V82 = struct
     let new_evi = Typeclasses.mark_unresolvable new_evi in
     let evk = Evarutil.new_untyped_evar () in
     let new_sigma = Evd.add Evd.empty evk new_evi in
-    { Evd.it = build evk ; sigma = new_sigma }
+    { Evd.it = build evk ; sigma = new_sigma; eff = Declareops.no_seff }
 
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index bb1c0639e..345f46abf 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -41,13 +41,15 @@ type subgoals = private { subgoals: goal list }
 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
+val eval :
+  'a sensitive -> Environ.env -> Evd.evar_map -> goal ->
+    'a * Evd.evar_map * Declareops.side_effects
 
 (* monadic bind on sensitive expressions *)
 val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive
 
 (* monadic return on sensitive expressions *)
-val return : 'a -> 'a sensitive
+val return : 'a -> Declareops.side_effects -> 'a sensitive
 
 
 (* interpretation of "open" constr *)
@@ -168,10 +170,10 @@ val here_list : goal list -> 'a -> 'a sensitive
 (* emulates List.map for functions of type 
    [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) -> 
-                        'a list -> 
-                        Evd.evar_map -> 
-                        'b list *Evd.evar_map
+val list_map : 
+  (Evd.evar_map -> 'a -> 'b * Evd.evar_map * Declareops.side_effects) ->
+  'a list -> Evd.evar_map ->
+    'b list * Evd.evar_map * Declareops.side_effects list
 
 (* 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 7dc3fb49a..68031e2b5 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -571,13 +571,12 @@ let prim_refiner r sigma goal =
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
 	      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'))
-		                              all sigma
+                let gl,ev,sig' =
+                  Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
+                (gl,ev),sig',Declareops.no_seff)
+              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
@@ -612,15 +611,14 @@ let prim_refiner r sigma goal =
               with
               |	Not_found ->
                   mk_sign (push_named_context_val (f,None,ar) sign) oth)
-	  | [] -> 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))
-	                                             all sigma                                      
+	  | [] -> 
+              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                                      
      	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 6132cc9c6..ed1de75bc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -26,49 +26,24 @@ let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let undo n =
-  let p = Proof_global.give_me_the_proof () in
-  let d = Proof.V82.depth p in
-  if n >= d then raise Proof.EmptyUndoStack;
-  for _i = 1 to n do
-    Proof.undo p
-  done
-
-let current_proof_depth () =
-  try
-    let p = Proof_global.give_me_the_proof () in
-    Proof.V82.depth p
-  with Proof_global.NoCurrentProof -> -1
-
-(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
-   is the depth of the focus stack). *)
-let undo_todepth n =
-  try
-    undo ((current_proof_depth ()) - n )
-  with Proof_global.NoCurrentProof  when Int.equal n 0 -> ()
+let set_undo _ = ()
+let get_undo _ = None
 
-let start_proof id str hyps c ?init_tac ?compute_guard hook = 
+let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
   let goals = [ (Global.env_of_context hyps , c) ] in
   Proof_global.start_proof id str goals ?compute_guard hook;
-  let tac = match init_tac with
-   | Some tac -> Proofview.V82.tactic tac
-   | None -> Proofview.tclUNIT ()
-  in
-  try Proof_global.run_tactic tac
-  with reraise ->
-    let reraise = Errors.push reraise in
-    Proof_global.discard_current ();
-    raise reraise
-
-let restart_proof () = undo_todepth 1
-
-let cook_proof hook =
-  let prf = Proof_global.give_me_the_proof () in
-  hook prf;
-  match Proof_global.close_proof () with
+  let env = Global.env () in
+  Proof_global.with_current_proof (fun _ p ->
+    match init_tac with
+    | None -> p
+    | Some tac -> Proof.run_tactic env (Proofview.V82.tactic tac) p)
+
+let cook_this_proof hook p =
+  match p with
   | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
+let cook_proof hook = cook_this_proof hook (Proof_global.close_proof ())
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
@@ -88,15 +63,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 } = Proof.V82.subgoals p in
+  let { it=goals ; sigma = sigma; eff = eff } = Proof.V82.subgoals p in
   try
-    { it=(List.nth goals (i-1)) ; sigma=sigma }
+          { it=(List.nth goals (i-1)) ; sigma=sigma; eff = eff }
   with Failure _ -> raise NoSuchGoal
     
 let get_goal_context_gen i =
   try
-    let { it=goal ; sigma=sigma } =  get_nth_V82_goal i in
-    (sigma, Refiner.pf_env { it=goal ; sigma=sigma })
+let { it=goal ; sigma=sigma; eff=eff } =  get_nth_V82_goal i in
+(sigma, Refiner.pf_env { it=goal ; sigma=sigma; eff=eff })
   with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
 
 let get_goal_context i =
@@ -115,26 +90,23 @@ let current_proof_statement () =
     | (id,([concl],strength,hook)) -> id,strength,concl,hook
     | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
 
-let solve_nth ?(with_end_tac=false) gi tac = 
+let solve_nth ?with_end_tac gi tac pr =
   try 
     let tac = Proofview.V82.tactic tac in
-    let tac = if with_end_tac then 
-                Proof_global.with_end_tac tac
-              else
-		tac
-    in
-    Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) 
-  with 
+    let tac = match with_end_tac with
+      | None -> tac
+      | Some etac -> Proofview.tclTHEN tac etac in
+    Proof.run_tactic (Global.env ()) (Proofview.tclFOCUS gi gi tac) pr
+  with
     | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
     | Proofview.IndexOutOfRange ->
 	let msg = str "No such goal: " ++ int gi ++ str "." in
 	Errors.errorlabstrm "" msg
 
-let by = solve_nth 1
+let by tac = Proof_global.with_current_proof (fun _ -> solve_nth 1 tac)
 
 let instantiate_nth_evar_com n com = 
-  let pf = Proof_global.give_me_the_proof () in
-  Proof.V82.instantiate_evar n com pf
+  Proof_global.with_current_proof (fun _ -> Proof.V82.instantiate_evar n com)
 
 
 (**********************************************************************)
@@ -144,8 +116,8 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id sign typ tac =
-  start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
+let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
+  start_proof id goal_kind sign typ (fun _ _ -> ());
   try
     by tac;
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
@@ -155,10 +127,19 @@ let build_constant_by_tactic id sign typ tac =
     delete_current_proof ();
     raise reraise
 
+let constr_of_def = function
+  | Declarations.Undef _ -> assert false
+  | Declarations.Def cs -> Lazyconstr.force cs
+  | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc)
+
 let build_by_tactic env typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  (build_constant_by_tactic id sign typ tac).const_entry_body
+  let ce = build_constant_by_tactic id sign typ tac in
+  let ce = Term_typing.handle_side_effects env ce in
+  let cb, se = Future.force ce.const_entry_body in
+  assert(se = Declareops.no_seff);
+  cb
 
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 976ac276e..ed9b55ae5 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -50,21 +50,6 @@ val delete_current_proof : unit -> unit
 val delete_all_proofs : unit -> unit
 
 (** {6 ... } *)
-(** [undo n] undoes the effect of the last [n] tactics applied to the
-    current proof; it fails if no proof is focused or if the ``undo''
-    stack is exhausted *)
-
-val undo : int -> unit
-
-(** [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
-   is the depth of the undo stack). *)
-val undo_todepth : int -> unit 
-
-(** Returns the depth of the current focused proof stack, this is used
-   to put informations in coq prompt (in emacs mode). *)
-val current_proof_depth: unit -> int
-
-(** {6 ... } *)
 (** [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
     proof end (e.g. to declare the built constructions as a coercion
@@ -79,17 +64,22 @@ val start_proof :
   ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
   unit declaration_hook -> unit
 
-(** [restart_proof ()] restarts the current focused proof from the beginning
-   or fails if no proof is focused *)
-
-val restart_proof : unit -> unit
-
 (** {6 ... } *)
 (** [cook_proof opacity] turns the current proof (assumed completed) into
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed;
     it also tells if the guardness condition has to be inferred. *)
 
+val cook_this_proof : (Proof.proof -> unit) ->
+    Id.t *
+    (Entries.definition_entry list *
+    lemma_possible_guards *
+    Decl_kinds.goal_kind *
+    unit Tacexpr.declaration_hook) ->
+  Id.t *
+    (Entries.definition_entry * lemma_possible_guards * goal_kind *
+     unit declaration_hook)
+
 val cook_proof : (Proof.proof -> unit) ->
   Id.t *
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
@@ -145,7 +135,8 @@ val get_used_variables : unit -> Context.section_context option
    current focused proof or raises a UserError if no proof is focused or
    if there is no [n]th subgoal *)
 
-val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit
+val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> tactic ->
+      Proof.proof -> Proof.proof
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
    focused proof or raises a UserError if there is no focused proof or
@@ -162,8 +153,9 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 
 (** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
 
-val build_constant_by_tactic : Id.t -> named_context_val -> types -> tactic ->
-  Entries.definition_entry
+val build_constant_by_tactic :
+  Id.t -> named_context_val -> ?goal_kind:goal_kind ->
+    types -> tactic -> Entries.definition_entry
 val build_by_tactic : env -> types -> tactic -> constr
 
 (** Declare the default tactic to fill implicit arguments *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 6cc43de72..38886e9e1 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -38,7 +38,7 @@ type unfocusable =
   | Cannot of exn
   | Loose
   | Strict
-type _focus_condition = 
+type _focus_condition =
     (_focus_kind -> Proofview.proofview -> unfocusable) *
     (_focus_kind -> bool)
 type 'a focus_condition = _focus_condition
@@ -83,11 +83,11 @@ module Cond = struct
     else c
   let (&&&) c1 c2 k p=
     match c1 k p , c2 k p with
-    | Cannot e , _ 
+    | Cannot e , _
     | _ , Cannot e -> Cannot e
     | Strict, Strict -> Strict
     | _ , _ -> Loose
-  let kind e k0 k p = bool e (Int.equal k0 k) k p 
+  let kind e k0 k p = bool e (Int.equal k0 k) k p
   let pdone e k p = bool e (Proofview.finished p) k p
 end
 
@@ -116,7 +116,7 @@ let done_cond ?loose_end = done_cond_gen CannotUnfocusThisWay ?loose_end
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
-type proof_state = {
+type proof = {
   (* Current focused proofview *)
   proofview: Proofview.proofview;
   (* History of the focusings, provides information on how
@@ -125,29 +125,9 @@ type proof_state = {
   focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list;
 }
 
-type proof_info = {
-  mutable endline_tactic : unit Proofview.tactic ;
-  mutable section_vars : Context.section_context option;
-  initial_conclusions : Term.types list
-}
-
-type undo_action = 
-  | State of proof_state
-  | Effect of (unit -> unit)
-
-type proof = { (* current proof_state *)
-               mutable state : proof_state;
-               (* The undo stack *)
-               mutable undo_stack : undo_action list;
-	       (* secondary undo stacks used for transactions *)
-	       mutable transactions : undo_action list list;
-	       info : proof_info
-             }
-
-
 (*** General proof functions ***)
 
-let proof { state = p } =
+let proof p =
   let (goals,sigma) = Proofview.proofview p.proofview in
   (* spiwack: beware, the bottom of the stack is used by [Proof]
      internally, and should not be exposed. *)
@@ -169,25 +149,22 @@ let rec unroll_focus pv = function
    doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
 let is_done p =
-  Proofview.finished p.state.proofview && 
-  Proofview.finished (unroll_focus p.state.proofview p.state.focus_stack)
+  Proofview.finished p.proofview &&
+  Proofview.finished (unroll_focus p.proofview p.focus_stack)
 
 (* spiwack: for compatibility with <= 8.2 proof engine *)
 let has_unresolved_evar p =
-  Proofview.V82.has_unresolved_evar p.state.proofview
+  Proofview.V82.has_unresolved_evar p.proofview
 
 (* Returns the list of partial proofs to initial goals *)
-let partial_proof p =
-  List.map fst (Proofview.return p.state.proofview)
-
-
+let partial_proof p = Proofview.partial_proof p.proofview
 
 (*** The following functions implement the basic internal mechanisms
      of proofs, they are not meant to be exported in the .mli ***)
 
 (* An auxiliary function to push a {!focus_context} on the focus stack. *)
 let push_focus cond inf context pr =
-  pr.state <- { pr.state with focus_stack = (cond,inf,context)::pr.state.focus_stack }
+  { pr with focus_stack = (cond,inf,context)::pr.focus_stack }
 
 exception FullyUnfocused
 let _ = Errors.register_handler begin function
@@ -196,162 +173,52 @@ let _ = Errors.register_handler begin function
 end
 (* An auxiliary function to read the kind of the next focusing step *)
 let cond_of_focus pr =
-  match pr.state.focus_stack with
+  match pr.focus_stack with
   | (cond,_,_)::_ -> cond
   | _ -> raise FullyUnfocused
 
 (* An auxiliary function to pop and read the last {!Proofview.focus_context} 
    on the focus stack. *)
 let pop_focus pr =
-  match pr.state.focus_stack with
-  | focus::other_focuses -> 
-      pr.state <- { pr.state with focus_stack = other_focuses }; focus
-  | _ -> 
+  match pr.focus_stack with
+  | focus::other_focuses ->
+      { pr with focus_stack = other_focuses }, focus
+  | _ ->
       raise FullyUnfocused
 
-(* Auxiliary function to push a [proof_state] onto the undo stack. *)
-let push_undo save pr =
-  match pr.transactions with
-  | [] -> pr.undo_stack <- save::pr.undo_stack
-  | stack::trans' -> pr.transactions <- (save::stack)::trans'
-
-(* Auxiliary function to pop and read a [save_state] from the undo stack. *)
-exception EmptyUndoStack
-let _ = Errors.register_handler begin function
-  | EmptyUndoStack -> Errors.error "Cannot undo: no more undo information"
-  | _ -> raise Errors.Unhandled
-end
-let pop_undo pr =
-  match pr.transactions , pr.undo_stack with
-  | [] , state::stack -> pr.undo_stack <- stack; state
-  | (state::stack)::trans', _ -> pr.transactions <- stack::trans'; state
-  | _ -> raise EmptyUndoStack
-
-
 (* This function focuses the proof [pr] between indices [i] and [j] *)
 let _focus cond inf i j pr =
-  let (focused,context) = Proofview.focus i j pr.state.proofview in
-  push_focus cond inf context pr;
-  pr.state <- { pr.state with proofview = focused }
+  let focused, context = Proofview.focus i j pr.proofview in
+  let pr = push_focus cond inf context pr in
+  { pr with proofview = focused }
 
 (* This function unfocuses the proof [pr], it raises [FullyUnfocused],
    if the proof is already fully unfocused.
    This function does not care about the condition of the current focus. *)
 let _unfocus pr =
-  let (_,_,fc) = pop_focus pr in
-  pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview }
-
-
-let set_used_variables l p =
-  p.info.section_vars <- Some l
-
-let get_used_variables p = p.info.section_vars
-
-(*** Endline tactic ***)
-
-(* spiwack this is an information about the UI, it might be a good idea to move
-   it to the Proof_global module *)
-
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac p =
- p.info.endline_tactic <- tac
-
-let with_end_tac pr tac =
-  Proofview.tclTHEN tac pr.info.endline_tactic
-
-(*** The following functions define the safety mechanism of the
-     proof system, they may be unsafe if not used carefully. There is
-     currently no reason to export them in the .mli ***)
-
-(* This functions saves the current state into a [proof_state]. *)
-let save_state { state = ps } = State ps
-
-(* This function stores the current proof state in the undo stack. *)
-let save pr =
-  push_undo (save_state pr) pr
-
-(* This function restores a state, presumably from the top of the undo stack. *)
-let restore_state save pr =
-  match save with
-  | State save -> pr.state <- save
-  | Effect undo -> undo ()
-
-(* Interpretes the Undo command. *)
-let undo pr =
-  (* On a single line, since the effects commute *)
-  restore_state (pop_undo pr) pr
-
-(* Adds an undo effect to the undo stack. Use it with care, errors here might result
-    in inconsistent states. *)
-let add_undo effect pr =
-  push_undo (Effect effect) pr
-
-
-
-(*** Transactions ***)
-
-let init_transaction pr =
-  pr.transactions <- []::pr.transactions
-
-let commit_stack pr stack =
-  let push s = push_undo s pr in
-  List.iter push (List.rev stack)
-
-(* Invariant: [commit] should be called only when a transaction
-   is open. It closes the current transaction. *)
-let commit pr =
-  match pr.transactions with
-  | stack::trans' ->
-    pr.transactions <- trans';
-    commit_stack pr stack
-  | [] -> assert false
-
-(* Invariant: [rollback] should be called only when a transaction
-   is open. It closes the current transaction. *)
-let rec rollback pr =
-  try
-    undo pr;
-    rollback pr
-  with EmptyUndoStack ->
-    match pr.transactions with
-    | []::trans' -> pr.transactions <- trans'
-    | _ -> assert false
-
-
-let transaction pr t =
-  init_transaction pr;
-  try t (); commit pr
-  with reraise ->
-    let reraise = Errors.push reraise in
-    rollback pr; raise reraise
-
+  let pr, (_,_,fc) = pop_focus pr in
+   { pr with proofview = Proofview.unfocus fc pr.proofview }
 
 (* Focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
 let focus cond inf i pr =
-  save pr;
   _focus cond (Obj.repr inf) i i pr
 
 let rec unfocus kind pr () =
-  let starting_point = save_state pr in
   let cond = cond_of_focus pr in
-  match fst cond kind pr.state.proofview with
+  match fst cond kind pr.proofview with
   | Cannot e -> raise e
-  | Strict -> 
-    (_unfocus pr;
-     push_undo starting_point pr)
+  | Strict ->
+     let pr = _unfocus pr in
+     pr
   | Loose ->
     begin try
-	    _unfocus pr;
-	    push_undo starting_point pr;
+            let pr = _unfocus pr in
 	    unfocus kind pr ()
       with FullyUnfocused -> raise CannotUnfocusThisWay
     end
 
-let unfocus kind pr =
-  transaction pr (unfocus kind pr)
-
 exception NoSuchFocus
 (* no handler: should not be allowed to reach toplevel. *)
 let rec get_in_focus_stack kind stack =
@@ -361,14 +228,20 @@ let rec get_in_focus_stack kind stack =
       else get_in_focus_stack kind stack
   | [] -> raise NoSuchFocus
 let get_at_focus kind pr =
-  Obj.magic (get_in_focus_stack kind pr.state.focus_stack)
+  Obj.magic (get_in_focus_stack kind pr.focus_stack)
 
 let is_last_focus kind pr =
-  let ((_,check),_,_) = List.hd pr.state.focus_stack in
+  let ((_,check),_,_) = List.hd pr.focus_stack in
   check kind
 
 let no_focused_goal p =
-  Proofview.finished p.state.proofview
+  Proofview.finished p.proofview
+
+let rec maximal_unfocus k p =
+  if no_focused_goal p then
+    try maximal_unfocus k (unfocus k p ())
+    with FullyUnfocused | CannotUnfocusThisWay -> p
+  else p
 
 (*** Proof Creation/Termination ***)
 
@@ -379,18 +252,10 @@ let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
 let unfocused = is_last_focus end_of_stack_kind
 
 let start goals =
-  let pr =
-    { state = { proofview = Proofview.init goals ;
-	        focus_stack = [] };
-      undo_stack = [] ;
-      transactions = [] ;
-      info = { endline_tactic = Proofview.tclUNIT ();
-               initial_conclusions = List.map snd goals;
-               section_vars = None }
-    }
-  in
-  _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr;
-  pr
+  let pr = {
+    proofview = Proofview.init goals ;
+    focus_stack = [] } in
+  _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 
 exception UnfinishedProof
 exception HasUnresolvedEvar
@@ -399,73 +264,64 @@ let _ = Errors.register_handler begin function
   | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
   | _ -> raise Errors.Unhandled
 end
-let return p =
+
+let return p t =
   if not (is_done p) then
     raise UnfinishedProof
-  else if has_unresolved_evar p then 
+  else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
     raise HasUnresolvedEvar
   else
-    unfocus end_of_stack_kind p;
-    Proofview.return p.state.proofview
+    let p = unfocus end_of_stack_kind p () in
+    Proofview.return p.proofview t
+
+let initial_goals p = Proofview.initial_goals p.proofview
+
+(*** Function manipulation proof extra informations ***)
 
 (*** Tactics ***)
 
 let run_tactic env tac pr =
-  let starting_point = save_state pr in
-  let sp = pr.state.proofview in
-  try
-    let tacticced_proofview = Proofview.apply env tac sp in
-    pr.state <- { pr.state with proofview = tacticced_proofview };
-    push_undo starting_point pr
-  with reraise ->
-    restore_state starting_point pr;
-    raise reraise
+  let sp = pr.proofview in
+  let tacticced_proofview = Proofview.apply env tac sp in
+  { pr with proofview = tacticced_proofview }
 
-(*** Commands ***)
+let emit_side_effects eff pr =
+  {pr with proofview = Proofview.emit_side_effects eff pr.proofview}
 
-let in_proof p k =
-  Proofview.in_proofview p.state.proofview k
+(*** Commands ***)
 
+let in_proof p k = Proofview.in_proofview p.proofview k
 
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
   let subgoals p =
-    Proofview.V82.goals p.state.proofview
+    Proofview.V82.goals p.proofview
 
   let background_subgoals p =
-    Proofview.V82.goals (unroll_focus p.state.proofview p.state.focus_stack)
-
-  let get_initial_conclusions p = 
-    p.info.initial_conclusions
+    Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
 
-  let depth p = List.length p.undo_stack
-
-  let top_goal p = 
-    let { Evd.it=gls ; sigma=sigma } = 
-	Proofview.V82.top_goals p.state.proofview
+  let top_goal p =
+    let { Evd.it=gls ; sigma=sigma; eff=eff } =
+	Proofview.V82.top_goals p.proofview
     in
-    { Evd.it=List.hd gls ; sigma=sigma }
+    { Evd.it=List.hd gls ; sigma=sigma; eff=eff }
 
   let top_evars p =
-    Proofview.V82.top_evars p.state.proofview
+    Proofview.V82.top_evars p.proofview
 
   let grab_evars p =
     if not (is_done p) then
       raise UnfinishedProof
     else
-      save p;
-      p.state <- { p.state with proofview = Proofview.V82.grab p.state.proofview }
-    
+      { p with proofview = Proofview.V82.grab p.proofview }
+
 
     let instantiate_evar n com pr =
-      let starting_point = save_state pr in
-      let sp = pr.state.proofview in
+      let sp = pr.proofview in
       try
 	let new_proofview = Proofview.V82.instantiate_evar n com sp in
-	pr.state <- { pr.state with proofview = new_proofview };
-	push_undo starting_point pr
-      with reraise ->
-	restore_state starting_point pr;
-	raise reraise
+        { pr with proofview = new_proofview }
+      with e ->
+	raise e
 end
diff --git a/proofs/proof.mli b/proofs/proof.mli
index b563452a9..70615e09e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -47,6 +47,7 @@ val proof : proof -> Goal.goal list * (Goal.goal list * Goal.goal list) list * E
 (*** General proof functions ***)
 
 val start : (Environ.env * Term.types) list -> proof
+val initial_goals : proof -> (Term.constr * Term.types) list
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
@@ -60,20 +61,8 @@ 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.types) list
-
-(* Interpretes the Undo command. Raises [EmptyUndoStack] if 
-    the undo stack is empty. *)
-exception EmptyUndoStack
-val undo : proof -> unit
-
-(* Adds an undo effect to the undo stack. Use it with care, errors here might result
-    in inconsistent states.
-   An undo effect is meant to undo an effect on a proof (a canonical example
-   of which is {!Proofglobal.set_proof_mode} which changes the current parser for
-   tactics). Make sure it will work even if the effects have been only partially
-   applied at the time of failure. *)
-val add_undo : (unit -> unit) -> proof -> unit
+val return :
+  proof -> Term.constr -> Term.constr * Declareops.side_effects
 
 (*** Focusing actions ***)
 
@@ -113,7 +102,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 (* focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
-val focus : 'a focus_condition -> 'a -> int -> proof -> unit
+val focus : 'a focus_condition -> 'a -> int -> proof -> proof
 
 exception FullyUnfocused
 exception CannotUnfocusThisWay
@@ -121,7 +110,7 @@ exception CannotUnfocusThisWay
    Raises [FullyUnfocused] if the proof is not focused.
    Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
      is not met. *)
-val unfocus : 'a focus_kind -> proof -> unit
+val unfocus : 'a focus_kind -> proof -> unit -> proof
 
 (* [unfocused p] returns [true] when [p] is fully unfocused. *)
 val unfocused : proof -> bool
@@ -138,34 +127,13 @@ val is_last_focus : 'a focus_kind -> proof -> bool
 (* returns [true] if there is no goal under focus. *)
 val no_focused_goal : proof -> bool
 
-(* Sets the section variables assumed by the proof *)
-val set_used_variables : Context.section_context -> proof -> unit
-val get_used_variables : proof -> Context.section_context option
-
-(*** Endline tactic ***)
-
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : unit Proofview.tactic -> proof -> unit
-
-val with_end_tac : proof -> unit Proofview.tactic -> unit Proofview.tactic
-
 (*** Tactics ***)
 
-val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
-
+val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof
 
-(*** Transactions ***)
-
-(* A transaction chains several commands into a single one. For instance,
-   a focusing command and a tactic. Transactions are such that if
-   any of the atomic action fails, the whole transaction fails.
-
-   During a transaction, the visible undo stack is constituted only
-   of the actions performed done during the transaction.
-
-   [transaction p f] can be called on an [f] using, itself, [transaction p].*)
-val transaction : proof -> (unit -> unit) -> unit
+val emit_side_effects : Declareops.side_effects -> proof -> proof
 
+val maximal_unfocus : 'a focus_kind -> proof -> proof
 
 (*** Commands ***)
 
@@ -178,19 +146,15 @@ module V82 : sig
   (* All the subgoals of the proof, including those which are not focused. *)
   val background_subgoals : proof -> Goal.goal list Evd.sigma
 
-  val get_initial_conclusions : proof -> Term.types list 
-
-  val depth : proof -> int 
-
   val top_goal : proof -> Goal.goal Evd.sigma
-  
+
   (* returns the existential variable used to start the proof *)
   val top_evars : proof -> Evd.evar list
 
   (* Turns the unresolved evars into goals.
      Raises [UnfinishedProof] if there are still unsolved goals. *)
-  val grab_evars : proof -> unit
+  val grab_evars : proof -> proof
 
   (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> unit
+  val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof
 end
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ed985f292..0c0aac715 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -17,6 +17,7 @@
 open Util
 open Pp
 open Names
+open Util
 
 (*** Proof Modes ***)
 
@@ -59,32 +60,31 @@ let _ =
 
 (*** Proof Global Environment ***)
 
-(* local shorthand *)
-type nproof = Id.t*Proof.proof
-
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_info = {
-  strength : Decl_kinds.goal_kind ;
-  compute_guard :  lemma_possible_guards;
-  hook : unit Tacexpr.declaration_hook ;
-  mode : proof_mode
+
+type pstate = {
+  pid : Id.t;
+  endline_tactic : unit Proofview.tactic;
+  section_vars : Context.section_context option;
+  proof : Proof.proof;
+  strength : Decl_kinds.goal_kind;
+  compute_guard : lemma_possible_guards;
+  hook : unit Tacexpr.declaration_hook;
+  mode : proof_mode;
 }
 
-(* Invariant: the domain of proof_info is current_proof.*)
-(* The head of [!current_proof] is the actual current proof, the other ones are
+(* The head of [!pstates] is the actual current proof, the other ones are
    to be resumed when the current proof is closed or aborted. *)
-let current_proof = ref ([]:nproof list)
-let proof_info = ref (Id.Map.empty : proof_info Id.Map.t)
+let pstates = ref ([] : pstate list)
 
 (* Current proof_mode, for bookkeeping *)
 let current_proof_mode = ref !default_proof_mode
 
 (* combinators for proof modes *)
 let update_proof_mode () =
-  match !current_proof with
-  | (id,_)::_ ->
-      let { mode = m } = Id.Map.find id !proof_info in
+  match !pstates with
+  | { mode = m } :: _ ->
       !current_proof_mode.reset ();
       current_proof_mode := m;
       !current_proof_mode.set ()
@@ -103,7 +103,7 @@ let _ = Errors.register_handler begin function
 end
 let extract id l =
   let rec aux = function
-    | ((id',_) as np)::l when Id.equal id id' -> (np,l)
+    | ({pid = id' } as np)::l when Id.equal id id' -> (np,l)
     | np::l -> let (np', l) = aux l in (np' , np::l)
     | [] -> raise NoSuchProof
   in
@@ -121,10 +121,6 @@ let extract_top l =
   match !l with
   | np::l' -> l := l' ; update_proof_mode (); np
   | [] -> raise NoCurrentProof
-let find_top l =
-  match !l with
-  | np::_ -> np
-  | [] -> raise NoCurrentProof
 
 (* combinators for the proof_info map *)
 let add id info m =
@@ -135,13 +131,28 @@ let remove id m =
 (*** Proof Global manipulation ***)
 
 let get_all_proof_names () =
-    List.map fst !current_proof
+  List.map (function { pid = id } -> id) !pstates
 
-let give_me_the_proof () =
-  snd (find_top current_proof)
+let cur_pstate () =
+  match !pstates with
+  | np::_ -> np
+  | [] -> raise NoCurrentProof
 
-let get_current_proof_name () =
-  fst (find_top current_proof)
+let give_me_the_proof () = (cur_pstate ()).proof
+let get_current_proof_name () = (cur_pstate ()).pid
+
+let with_current_proof f =
+  match !pstates with
+  | [] -> raise NoCurrentProof
+  | p :: rest ->
+      let p = { p with proof = f p.endline_tactic p.proof } in
+      pstates := p :: rest
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac =
+  match !pstates with
+  | [] -> raise NoCurrentProof
+  | p :: rest -> pstates := { p with endline_tactic = tac } :: rest
 
 (* spiwack: it might be considered to move error messages away.
     Or else to remove special exceptions from Proof_global.
@@ -155,7 +166,7 @@ let msg_proofs () =
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
                (pr_sequence Nameops.pr_id l) ++ str".")
 
-let there_is_a_proof () = not (List.is_empty !current_proof)
+let there_is_a_proof () = not (List.is_empty !pstates)
 let there_are_pending_proofs () = there_is_a_proof ()
 let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
@@ -167,51 +178,40 @@ let check_no_pending_proof () =
   end
 
 let discard_gen id =
-  ignore (extract id current_proof);
-  remove id proof_info
+  pstates := List.filter (fun { pid = id' } -> id <> id') !pstates
 
 let discard (loc,id) =
-  try
-    discard_gen id
-  with NoSuchProof ->
+  let n = List.length !pstates in
+  discard_gen id;
+  if List.length !pstates = n then
     Errors.user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
-  let (id,_) = extract_top current_proof in
-  remove id proof_info
+  if !pstates = [] then raise NoCurrentProof else pstates := List.tl !pstates
 
-let discard_all () =
-  current_proof := [];
-  proof_info := Id.Map.empty
+let discard_all () = pstates := []
 
 (* [set_proof_mode] sets the proof mode to be used after it's called. It is
     typically called by the Proof Mode command. *)
-(* Core component.
-    No undo handling.
-    Applies to proof [id], and proof mode [m]. *)
 let set_proof_mode m id =
-  let info = Id.Map.find id !proof_info in
-  let info = { info with mode = m } in
-  proof_info := Id.Map.add id info !proof_info;
+  pstates :=
+    List.map (function { pid = id' } as p ->
+      if Id.equal id' id then { p with mode = m } else p) !pstates;
   update_proof_mode ()
-(* Complete function.
-    Handles undo.
-    Applies to current proof, and proof mode name [mn]. *)
+
 let set_proof_mode mn =
-  let m = find_proof_mode mn in
-  let id = get_current_proof_name () in
-  let pr = give_me_the_proof () in
-  Proof.add_undo begin let curr = !current_proof_mode in fun () ->
-    set_proof_mode curr id ; update_proof_mode ()
-  end pr ;
-  set_proof_mode m id
+  set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
+
+let activate_proof_mode mode = (find_proof_mode mode).set ()
+let disactivate_proof_mode mode = (find_proof_mode mode).reset ()
 
 exception AlreadyExists
 let _ = Errors.register_handler begin function
   | AlreadyExists -> Errors.error "Already editing something of that name."
   | _ -> raise Errors.Unhandled
 end
+
 (* [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
     proof end (e.g. to declare the built constructions as a coercion
@@ -220,84 +220,67 @@ end
     proof of mutually dependent theorems).
     It raises exception [ProofInProgress] if there is a proof being
     currently edited. *)
-let start_proof  id str goals ?(compute_guard=[]) hook =
-  begin
-    List.iter begin fun (id_ex,_) ->
-      if Names.Id.equal id id_ex then raise AlreadyExists
-    end !current_proof
-  end;
-  let p = Proof.start goals in
-  add id { strength=str ;
-	        compute_guard=compute_guard ;
-		hook=hook ;
-	        mode = ! default_proof_mode } proof_info ;
-  push (id,p) current_proof
-
-(* arnaud: à enlever *)
-let run_tactic tac =
-  let p = give_me_the_proof () in
-  let env = Global.env () in
-  Proof.run_tactic env tac p
 
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac =
-  let p = give_me_the_proof () in
-  Proof.set_endline_tactic tac p
+let start_proof id str goals ?(compute_guard=[]) hook =
+  let initial_state = {
+    pid = id;
+    proof = Proof.start goals;
+    endline_tactic = Proofview.tclUNIT ();
+    section_vars = None;
+    strength = str;
+    compute_guard = compute_guard;
+    hook = hook;
+    mode = ! default_proof_mode } in
+  push initial_state pstates
+
+let get_used_variables () = (cur_pstate ()).section_vars
 
 let set_used_variables l =
-  let p = give_me_the_proof () in
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
-  Proof.set_used_variables ctx p
-
-let get_used_variables () =
-  Proof.get_used_variables (give_me_the_proof ())
-
-let with_end_tac tac =
-  let p = give_me_the_proof () in
-  Proof.with_end_tac p tac
-
+  match !pstates with
+  | [] -> raise NoCurrentProof
+  | p :: rest ->
+      if p.section_vars <> None then
+        Errors.error "Used section variables can be declared only once";
+      pstates := { p with section_vars = Some ctx} :: rest
+
+let get_open_goals () =
+  let gl, gll, _ = Proof.proof (cur_pstate ()).proof in
+  List.length gl +
+  List.fold_left (+) 0
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll)
+
+type closed_proof =
+  Names.Id.t *
+  (Entries.definition_entry list * lemma_possible_guards *
+    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+
+let close_proof ~now ?(fix_exn = fun x -> x) ps side_eff =
+  let { pid; section_vars; compute_guard; strength; hook; proof } = ps in
+  let entries = List.map (fun (c, t) -> { Entries.
+    const_entry_body = Future.chain side_eff (fun () ->
+      try Proof.return (cur_pstate ()).proof c 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"))));
+    const_entry_secctx = section_vars;
+    const_entry_type  = Some t;
+    const_entry_inline_code = false;
+    const_entry_opaque = true }) (Proof.initial_goals proof) in
+  if now then
+    List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
+  (pid, (entries, compute_guard, strength, hook))
+
+let close_future_proof ~fix_exn proof =
+  close_proof ~now:false ~fix_exn (cur_pstate ()) proof
 let close_proof () =
-  (* spiwack: for now close_proof doesn't actually discard the proof, it is done
-      by [Command.save]. *)
-  try
-    let id = get_current_proof_name () in
-    let p = give_me_the_proof () in
-    let proofs_and_types = Proof.return p in
-    let section_vars = Proof.get_used_variables p in
-    let entries = List.map
-      (fun (c,t) -> { Entries.const_entry_body = c;
-                      const_entry_secctx = section_vars;
-                      const_entry_type = Some t;
-              const_entry_opaque = true;
-              const_entry_inline_code = false })
-      proofs_and_types
-    in
-    let { compute_guard=cg ; strength=str ; hook=hook } =
-      Id.Map.find id !proof_info
-    in
-    (id, (entries,cg,str,hook))
-  with
-    |  Proof.UnfinishedProof ->
-	 Errors.error "Attempt to save an incomplete proof"
-    | Proof.HasUnresolvedEvar ->
-	Errors.error "Attempt to save a proof with existential variables still non-instantiated"
-
-
-(**********************************************************)
-(*                                                                                                  *)
-(*                              Utility functions                                          *)
-(*                                                                                                  *)
-(**********************************************************)
-
-let maximal_unfocus k p =
-  begin try while Proof.no_focused_goal p do
-    Proof.unfocus k p
-  done
-  with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> ()
-  end
-
+  close_proof ~now:true (cur_pstate ()) (Future.from_val())
 
 (**********************************************************)
 (*                                                        *)
@@ -317,7 +300,7 @@ module Bullet = struct
 
   type behavior = {
     name : string;
-    put : Proof.proof -> t -> unit
+    put : Proof.proof -> t -> Proof.proof
   }
 
   let behaviors = Hashtbl.create 4
@@ -326,7 +309,7 @@ module Bullet = struct
   (*** initial modes ***)
   let none = {
     name = "None";
-    put = fun _ _ -> ()
+    put = fun x _ -> x
   }
   let _ = register_behavior none
 
@@ -356,8 +339,8 @@ module Bullet = struct
     let pop pr =
       match get_bullets pr with
       | b::_ ->
-	Proof.unfocus bullet_kind pr;
-	(*returns*) b
+         let pr = Proof.unfocus bullet_kind pr () in
+         pr, b
       | _ -> assert false
 
     let push b pr =
@@ -365,10 +348,10 @@ module Bullet = struct
 
     let put p bul =
       if has_bullet bul p then
-	Proof.transaction p begin fun () ->
-	  while not (bullet_eq bul (pop p)) do () done;
-	  push bul p
-	end
+        let rec aux p =
+          let p, b = pop p in
+          if not (bullet_eq bul b) then aux p else p in
+        push bul (aux p)
       else
 	push bul p
 
@@ -403,11 +386,11 @@ end
 
 module V82 = struct
   let get_current_initial_conclusions () =
-    let p = give_me_the_proof () in
-    let id = get_current_proof_name () in
-    let { strength=str ; hook=hook } =
-      Id.Map.find id !proof_info
-    in
-    (id,(Proof.V82.get_initial_conclusions p, str, hook))
+    let { pid; strength; hook; proof } = cur_pstate () in
+    pid, (List.map snd (Proof.initial_goals proof), strength, hook)
 end
 
+type state = pstate list
+let freeze () = !pstates
+let unfreeze s = pstates := s; update_proof_mode ()
+
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 7fa44cf86..a5fe33992 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -28,7 +28,6 @@ type proof_mode = {
     It corresponds to Coq default setting are they are set when coqtop starts. *)
 val register_proof_mode : proof_mode -> unit
 
-val there_is_a_proof : unit -> bool
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
@@ -60,18 +59,27 @@ val start_proof : Names.Id.t ->
                           unit Tacexpr.declaration_hook -> 
                           unit
 
-val close_proof : unit -> 
-                           Names.Id.t * 
-                          (Entries.definition_entry list * 
-			    lemma_possible_guards * 
-			    Decl_kinds.goal_kind * 
-			    unit Tacexpr.declaration_hook)
+type closed_proof =
+  Names.Id.t *
+  (Entries.definition_entry list * lemma_possible_guards *
+    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+
+val close_proof : unit -> closed_proof
+
+(* A future proof may be executed later on, out of the control of Stm
+   that knows which state was (for example) supposed to close the proof
+   bit did not. Hence fix_exn to enrich it *)
+val close_future_proof :
+  fix_exn:(exn -> exn) -> unit Future.computation -> closed_proof
 
 exception NoSuchProof
 
+val get_open_goals : unit -> int
+
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
    no current proof. *)
-val run_tactic : unit Proofview.tactic -> unit
+val with_current_proof :
+  (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : unit Proofview.tactic -> unit
@@ -80,18 +88,19 @@ val set_endline_tactic : unit Proofview.tactic -> unit
 val set_used_variables : Names.Id.t list -> unit
 val get_used_variables : unit -> Context.section_context option
 
-(** Appends the endline tactic of the current proof to a tactic. *)
-val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
+val discard : Names.identifier Loc.located -> unit
+val discard_current : unit -> unit
+val discard_all : unit -> unit
 
 (**********************************************************)
-(*                                                                                                  *)
-(*                              Utility functions                                          *)
-(*                                                                                                  *)
+(*                                                        *)
+(*                            Proof modes                 *)
+(*                                                        *)
 (**********************************************************)
 
-(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a
-    focused goal or that the last focus isn't of kind [k]. *)
-val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit
+
+val activate_proof_mode : string -> unit
+val disactivate_proof_mode : string -> unit
 
 (**********************************************************)
 (*                                                        *)
@@ -107,7 +116,7 @@ module Bullet : sig
       with a name to identify it. *)
   type behavior = {
     name : string;
-    put : Proof.proof -> t -> unit
+    put : Proof.proof -> t -> Proof.proof
   }
 
   (** A registered behavior can then be accessed in Coq
@@ -123,9 +132,13 @@ module Bullet : sig
 
   (** Handles focusing/defocusing with bullets:
        *)
-  val put : Proof.proof -> t -> unit
+  val put : Proof.proof -> t -> Proof.proof
 end
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
 end
+
+type state
+val freeze : unit -> state
+val unfreeze : state -> unit
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 45b7c084d..8a2c7617c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -26,7 +26,8 @@ open Util
 type proofview = {
      initial : (Term.constr * Term.types) list;
      solution : Evd.evar_map;
-     comb : Goal.goal list
+     comb : Goal.goal list;
+     side_effects : Declareops.side_effects
      }
 
 let proofview p =
@@ -38,7 +39,8 @@ let init =
   let rec aux = function
   | [] ->  { initial = [] ; 
 	     solution = Evd.empty ;
-	     comb = []
+             comb = [];
+             side_effects = Declareops.no_seff
 	   }
   | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
                            aux l
@@ -50,12 +52,15 @@ let init =
 			 let gl = Goal.build e in
 			 { initial = (econstr,typ)::ret;
 			   solution = new_defs ;
-			   comb = gl::comb }
+                           comb = gl::comb;
+                           side_effects = Declareops.no_seff }
   in
   fun l -> let v = aux l in
     (* Marks all the goal unresolvable for typeclasses. *)
     { v with solution = Typeclasses.mark_unresolvables v.solution }
 
+let initial_goals { initial } = initial
+
 (* Returns whether this proofview is finished or not. That is,
    if it has empty subgoals in the comb. There could still be unsolved
    subgoaled, but they would then be out of the view, focused out. *)
@@ -64,8 +69,13 @@ let finished = function
   | _  -> false
 
 (* Returns the current value of the proofview partial proofs. *)
-let return { initial=init; solution=defs }  =
-  List.map (fun (c,t) -> (Evarutil.nf_evar defs c , t)) init
+let return { solution=defs; side_effects=eff } c = Evarutil.nf_evar defs c, eff
+
+let partial_proof pv =
+  List.map fst (List.map (return 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 }
 
 (* spiwack: this function should probably go in the Util section,
     but I'd rather have Util (or a separate module for lists)
@@ -356,8 +366,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) = Goal.eval s env defs g in
-    (k a) , defs
+    let (a,defs,effs) = Goal.eval s env defs g in
+    (k a) , defs, effs
   end step.comb step.solution
 (* In form of a tactic *)
 let list_of_sensitive s k env =
@@ -366,8 +376,10 @@ let list_of_sensitive s k env =
   let (>>) = Inner.seq in
   Inner.get >>= fun step ->
   try 
-    let (tacs,defs) = list_of_sensitive s k env step in
-    Inner.set { step with solution = defs } >>
+    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) } >>
     Inner.return tacs
   with e when catchable_exception e ->
     tclZERO e env
@@ -388,19 +400,22 @@ 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) as partial_res) = 
+  let wrap g ((defs, partial_list, partial_eff) as partial_res) = 
     match Goal.advance defs g with
-    | None ->partial_res
+    | None -> partial_res
     | Some g ->
-      let {Goal.subgoals = sg } , d' = Goal.eval s env defs g in
-      (d',sg::partial_list)
+      let { Goal.subgoals = sg } , d', eff = Goal.eval s env defs g in
+      (d', sg::partial_list, eff::partial_eff)
   in
-  let ( new_defs , combed_subgoals ) = 
-    List.fold_right wrap step.comb (step.solution,[])
+  let ( new_defs , combed_subgoals, side_effects ) = 
+    List.fold_right wrap step.comb (step.solution,[],[])
   in
   { step with
      solution = new_defs;
-     comb = List.flatten combed_subgoals }
+     comb = List.flatten combed_subgoals;
+     side_effects =
+       Declareops.union_side_effects
+         (Declareops.flatten_side_effects side_effects) step.side_effects }
 let tclSENSITIVE s env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Inner.bind in
@@ -440,18 +455,26 @@ module V82 = struct
     Inner.get >>= fun ps ->
     try
       let tac evd gl = 
-        let glsigma  = tac { Evd.it = gl ; Evd.sigma = evd }  in
+        let glsigma  =
+          tac { Evd.it = gl ; sigma = evd; eff = Declareops.no_seff }  in
         let sigma = glsigma.Evd.sigma in
         let g = glsigma.Evd.it in
-        ( g , sigma )
+        ( g, sigma, glsigma.Evd.eff )
       in
     (* Old style tactics expect the goals normalized with respect to evars. *)
-      let (initgoals,initevd) = 
-        Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+      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
       in
-      let (goalss,evd) = Goal.list_map tac initgoals initevd in
+      let (goalss,evd,eff2) = Goal.list_map tac initgoals initevd in
       let sgs = List.flatten goalss in
-      Inner.set { ps with solution=evd ; comb=sgs }
+      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)) }
     with e when catchable_exception e ->
       tclZERO e env
 
@@ -471,12 +494,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 } = 
-    { Evd.it = comb ; sigma = solution}
+  let goals { comb = comb ; solution = solution; side_effects=eff } =
+   { Evd.it = comb ; sigma = solution; eff=eff}
 
-  let top_goals { initial=initial ; solution=solution } = 
+  let top_goals { initial=initial ; solution=solution; side_effects=eff } =
     let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
-    { Evd.it = goals ; sigma=solution }
+    { Evd.it = goals ; sigma=solution; eff=eff }
 
   let top_evars { initial=initial } =
     let evars_of_initial (c,_) =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index ff327ab3b..2869e75e1 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -44,8 +44,11 @@ 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*types) list
+val return : proofview -> constr -> constr * Declareops.side_effects
 
+val partial_proof : proofview -> constr list
+val initial_goals : proofview -> (constr * types) list
+val emit_side_effects : Declareops.side_effects -> proofview -> proofview
 
 (*** Focusing operations ***)
 
@@ -181,10 +184,6 @@ val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic
 
 val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
 
-
-
-
-
 (* Notations for building tactics. *)
 module Notations : sig
   (* Goal.bind *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index dfc9c0a63..06e35284d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -16,6 +16,7 @@ open Logic
 
 
 let sig_it x = x.it
+let sig_eff x = x.eff
 let project x = x.sigma
 
 (* Getting env *)
@@ -25,7 +26,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'}
+  { it = sgl; sigma = sigma'; eff = goal_sigma.eff }
 
 let norm_evar_tac gl = refiner (Change_evars) gl
 
@@ -34,18 +35,19 @@ let norm_evar_tac gl = refiner (Change_evars) gl
 (*********************)
 
 
-let unpackage glsig = (ref (glsig.sigma)),glsig.it
+let unpackage glsig = (ref (glsig.sigma)), glsig.it, (ref (glsig.eff))
 
-let repackage r v = {it=v;sigma = !r}
+let repackage e r v = {it = v; sigma = !r; eff = !e}
 
-let apply_sig_tac r tac g =
+let apply_sig_tac eff r tac g =
   check_for_interrupt (); (* Breakpoint *)
-  let glsigma = tac (repackage r g) in
+  let glsigma = tac (repackage eff 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}
+let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; eff=gls.eff}
 
 (* forces propagation of evar constraints *)
 let tclNORMEVAR = norm_evar_tac
@@ -69,35 +71,39 @@ 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) = unpackage gls in
-  (sigr,[g])
+  let sigr, g, eff = unpackage gls in
+  (sigr, [g], eff)
 
-let finish_tac (sigr,gl) = repackage sigr gl
+let finish_tac (sigr,gl,eff) = repackage eff 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) =
+let thens3parts_tac tacfi tac tacli (sigr,gs,eff) =
   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 sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
+        apply_sig_tac eff 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)
+    (sigr,List.flatten gll, eff)
 
 (* 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) =
+let thensi_tac tac (sigr,gs,eff) =
   let gll =
-    List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
-  (sigr, List.flatten gll)
+    List.map_i (fun i -> apply_sig_tac eff sigr (tac i)) 1 gs in
+  (sigr, List.flatten gll, eff)
 
 let then_tac tac = thensf_tac [||] tac
 
+let non_existent_goal n =
+  errorlabstrm ("No such goal: "^(string_of_int n))
+    (str"Trying to apply a tactic to a non existent goal")
+
 (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
@@ -192,9 +198,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} = rslt in
+  let {it=gls;sigma=sigma;eff=eff} = rslt in
   let hyps:Context.named_context list =
-    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma}) gls in
+    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; eff=eff}) gls in
   let newhyps =
     List.map (fun hypl -> List.subtract hypl oldhyps) hyps in
   let emacs_str s =
@@ -244,8 +250,8 @@ let tclORELSE_THEN t1 t2then t2else gls =
   with
     | None -> t2else gls
     | Some sgl ->
-        let (sigr,gl) = unpackage sgl in
-        finish_tac (then_tac t2then  (sigr,gl))
+        let sigr, gl, eff = unpackage sgl in
+        finish_tac (then_tac t2then  (sigr,gl,eff))
 
 (* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
 let tclTRY f = (tclORELSE0 f tclIDTAC)
@@ -350,23 +356,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 in
+  let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in
   if List.is_empty gl then error "first_goal";
-  { it = List.hd gl; sigma = sig_0 }
+  { it = List.hd gl; sigma = sig_0 ; eff = eff_0 }
 
 (* goal_goal_list : goal sigma -> goal list sigma *)
 
 let goal_goal_list gls =
-  let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 }
+  let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in 
+  { it = [gl]; sigma = sig_0; eff = eff_0 }
 
 (* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
 
 let apply_tac_list tac glls =
-  let (sigr,lg) = unpackage glls in
+  let (sigr,lg,eff) = unpackage glls in
   match lg with
   | (g1::rest) ->
-      let gl = apply_sig_tac sigr tac g1 in
-      repackage sigr (gl@rest)
+      let gl = apply_sig_tac eff sigr tac g1 in
+      repackage eff 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 c198958e3..b2e753ea3 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -16,15 +16,17 @@ 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
-val repackage : evar_map ref -> 'a -> '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 apply_sig_tac :
-  evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
+  Declareops.side_effects ref -> 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 813a0d850..fad46c99b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -22,7 +22,7 @@ open Proof_type
 open Logic
 open Refiner
 
-let re_sig it gc = { it = it; sigma = gc }
+let re_sig it eff  gc = { it = it; sigma = gc; eff = eff }
 
 (**************************************************************)
 (* Operations for handling terms under a local typing context *)
@@ -36,6 +36,7 @@ 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 1c0ab2d14..19eb9ba7c 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -27,14 +27,16 @@ 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 -> evar_map -> 'a sigma
+val re_sig : 'a -> Declareops.side_effects -> evar_map -> 'a sigma
 
-val unpackage : 'a sigma -> evar_map ref * 'a
-val repackage : evar_map ref -> 'a -> '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 apply_sig_tac :
-  evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) 
+  Declareops.side_effects ref -> evar_map ref -> 
+  (goal sigma -> (goal list) sigma) -> goal -> (goal list) 
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env