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

12 files changed, 136 insertions, 99 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fab324962b..29eb9e9ec8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -983,7 +983,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> Errors.error "No focused goal."
   | g::_ ->
-    let gl = { Evd.it = g; sigma = glss.Evd.sigma } in
+    let gl = { Evd.it = g; sigma = glss.Evd.sigma; eff = Declareops.no_seff } in
     pr_hint_term (pf_concl gl)
 
 (* displays the whole hint database db *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bfe80d7087..21678c9714 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -291,15 +291,16 @@ let make_autogoal_hints =
 	  unfreeze (Some (only_classes, sign, hints)); hints
 	  
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
-  { skft = fun sk fk {it = gl,hints; sigma=s} ->
-    let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
+  { skft = fun sk fk {it = gl,hints; sigma=s;eff=eff} ->
+    let res = try Some (tac {it=gl; sigma=s;eff=eff}) 
+              with e when catchable e -> None in
       match res with
       | Some gls -> sk (f gls hints) fk
       | None -> fk () }
 
 let intro_tac : atac =
   lift_tactic Tactics.intro
-    (fun {it = gls; sigma = s} info ->
+    (fun {it = gls; sigma = s;eff=eff} info ->
       let gls' =
 	List.map (fun g' ->
 	  let env = Goal.V82.env s g' in
@@ -308,13 +309,13 @@ let intro_tac : atac =
 	    (true,false,false) info.only_classes None (List.hd context) in
 	  let ldb = Hint_db.add_list hint info.hints in
 	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
-      in {it = gls'; sigma = s})
+      in {it = gls'; sigma = s;eff=eff})
 
 let normevars_tac : atac = 
-  { skft = fun sk fk {it = (gl, info); sigma = s} ->
+  { skft = fun sk fk {it = (gl, info); sigma = s; eff=eff} ->
     let gl', sigma' = Goal.V82.nf_evar s gl in
     let info' = { info with auto_last_tac = lazy (str"normevars") } in
-      sk {it = [gl', info']; sigma = sigma'} fk }
+      sk {it = [gl', info']; sigma = sigma';eff=eff} fk }
 
 (* Ordering of states is lexicographic on the number of remaining goals. *)
 let compare (pri, _, _, res) (pri', _, _, res') =
@@ -329,9 +330,9 @@ let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
   { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
 
 let hints_tac hints =
-  { skft = fun sk fk {it = gl,info; sigma = s} ->
+  { skft = fun sk fk {it = gl,info; sigma = s;eff=eff} ->
       let concl = Goal.V82.concl s gl in
-      let tacgl = {it = gl; sigma = s} in
+      let tacgl = {it = gl; sigma = s;eff=eff} in
       let poss = e_possible_resolve hints info.hints concl in
       let rec aux i foundone = function
 	| (tac, _, b, name, pp) :: tl ->
@@ -343,7 +344,7 @@ let hints_tac hints =
 	  in
 	    (match res with
 	       | None -> aux i foundone tl
-	       | Some {it = gls; sigma = s'} ->
+	       | Some {it = gls; sigma = s';eff=eff} ->
 	    	   if !typeclasses_debug then
 		     msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
 			    ++ str" on" ++ spc () ++ pr_ev s gl);
@@ -375,11 +376,11 @@ let hints_tac hints =
 			      hints =
 			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
 			      then make_autogoal_hints info.only_classes
-				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
+				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';eff=eff}
 			      else info.hints;
 			      auto_cut = derivs }
 			in g, info) 1 newgls in
-		   let glsv = {it = gls'; sigma = s'} in
+		   let glsv = {it = gls'; sigma = s';eff=eff} in
 		     sk glsv fk)
 	| [] ->
 	  if not foundone && !typeclasses_debug then
@@ -422,14 +423,14 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 		       fk)
 		    else fk'
 		  in aux s' (gls'::acc) fk'' gls)
-	       fk {it = (gl,info); sigma = s})
+	       fk {it = (gl,info); sigma = s; eff = Declareops.no_seff })
     | [] -> Somek2 (List.rev acc, s, fk)
-  in fun {it = gls; sigma = s} fk ->
+  in fun {it = gls; sigma = s; eff = eff} fk ->
     let rec aux' = function
       | Nonek2 -> fk ()
       | Somek2 (res, s', fk') ->
 	  let goals' = List.concat res in
-	    sk {it = goals'; sigma = s'} (fun () -> aux' (fk' ()))
+	    sk {it = goals'; sigma = s'; eff = eff } (fun () -> aux' (fk' ()))
     in aux' (aux s [] (fun () -> Nonek2) gls)
 
 let then_tac (first : atac) (second : atac) : atac =
@@ -468,8 +469,8 @@ let cut_of_hints h =
 let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
   let cut = cut_of_hints hints in
   { it = List.map_i (fun i g -> 
-    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'} in
-      (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
+    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'; eff = Declareops.no_seff } in
+      (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; eff = Declareops.no_seff }
 
 let get_result r = 
   match r with
@@ -494,11 +495,11 @@ let eauto_tac ?limit hints =
   | Some limit -> fix_limit limit (eauto_tac hints)
       
 let eauto ?(only_classes=true) ?st ?limit hints g =
-  let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g } in
+  let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; eff=g.eff } in
     match run_tac (eauto_tac ?limit hints) gl with
     | None -> raise Not_found
-    | Some {it = goals; sigma = s} ->
-	{it = List.map fst goals; sigma = s}
+    | Some {it = goals; sigma = s; eff=eff} ->
+	{it = List.map fst goals; sigma = s; eff=eff}
 
 let real_eauto st ?limit hints p evd =
   let rec aux evd fails =
@@ -544,7 +545,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
   let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) = 
     Goal.V82.mk_goal sigma nc gl Store.empty in
-  let gls = { it = gl ; sigma = sigma } in
+  let gls = { it = gl ; sigma = sigma; eff= Declareops.no_seff } in (* XXX eff *)
   let hints = searchtable_map typeclasses_db in
   let gls' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
   let evd = sig_sig gls' in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 62d13c0a65..9c020930c8 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -27,7 +27,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
        apropriate type *)
-    let cte = find_scheme kind ind in
+    let cte, eff = find_scheme kind ind in
     let c = mkConst cte in
     let t = type_of_constant (Global.env()) cte in
     let (mib,mip) = Global.lookup_inductive ind in
@@ -39,24 +39,24 @@ let optimize_non_type_induction_scheme kind dep sort ind =
 	mib.mind_nparams_rec
       else
 	mib.mind_nparams in
-    snd (weaken_sort_scheme (new_sort_in_family sort) npars c t)
+    snd (weaken_sort_scheme (new_sort_in_family sort) npars c t), eff
   else
-    build_induction_scheme (Global.env()) Evd.empty ind dep sort
+    build_induction_scheme (Global.env()) Evd.empty ind dep sort, Declareops.no_seff
 
 let build_induction_scheme_in_type dep sort ind =
   build_induction_scheme (Global.env()) Evd.empty ind dep sort
 
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (build_induction_scheme_in_type false InType)
+    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (build_induction_scheme_in_type false InType)
+    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (build_induction_scheme_in_type true InType)
+    (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
 
 let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
@@ -85,24 +85,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (build_case_analysis_scheme_in_type false InType)
+  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (build_case_analysis_scheme_in_type false InType)
+  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (build_case_analysis_scheme_in_type true InType)
+  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (build_case_analysis_scheme_in_type true InProp)
+  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (build_case_analysis_scheme_in_type true InType)
+  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (build_case_analysis_scheme_in_type true InProp)
+  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index cc11621681..7aac37d1b2 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -180,7 +180,7 @@ let build_sym_scheme env ind =
 
 let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
-  (fun ind -> build_sym_scheme (Global.env() (* side-effect! *)) ind)
+  (fun ind -> build_sym_scheme (Global.env() (* side-effect! *)) ind, Declareops.no_seff)
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -201,7 +201,8 @@ let sym_scheme_kind =
 let build_sym_involutive_scheme env ind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env ind in
-  let sym = mkConst (find_scheme sym_scheme_kind ind) in
+  let c, eff = find_scheme sym_scheme_kind ind in
+  let sym = mkConst c in
   let (eq,eqrefl) = get_coq_eq () in
   let cstr n = mkApp (mkConstruct(ind,1),extended_rel_vect n paramsctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
@@ -236,7 +237,8 @@ let build_sym_involutive_scheme env ind =
 	       [|mkRel 1|]])|]]);
 	 mkRel 1|])),
      mkRel 1 (* varH *),
-       [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+       [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))),
+  eff
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
@@ -305,8 +307,10 @@ let sym_involutive_scheme_kind =
 let build_l2r_rew_scheme dep env ind kind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env ind in
-  let sym = mkConst (find_scheme sym_scheme_kind ind) in
-  let sym_involutive = mkConst (find_scheme sym_involutive_scheme_kind ind) in
+  let c, eff = find_scheme sym_scheme_kind ind in
+  let sym = mkConst c in
+  let c, eff' = find_scheme sym_involutive_scheme_kind ind in
+  let sym_involutive = mkConst c in
   let (eq,eqrefl) = get_coq_eq () in
   let cstr n p =
     mkApp (mkConstruct(ind,1),
@@ -384,7 +388,8 @@ let build_l2r_rew_scheme dep env ind kind =
          Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
        [|main_body|])
    else
-     main_body))))))
+     main_body)))))),
+  Declareops.union_side_effects eff' eff
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -613,7 +618,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType)
+  (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -623,7 +628,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
+  (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -633,7 +638,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType)
+  (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -647,7 +652,7 @@ let rew_l2r_forward_dep_scheme_kind =
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun ind -> fix_r2l_forward_rew_scheme
-      (build_r2l_forward_rew_scheme false (Global.env()) ind InType))
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -657,7 +662,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType)
+  (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
 
 (* End of rewriting schemes *)
 
@@ -728,4 +733,4 @@ let build_congr env (eq,refl) ind =
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun ind ->
     (* May fail if equality is not defined *)
-    build_congr (Global.env()) (get_coq_eq ()) ind)
+          build_congr (Global.env()) (get_coq_eq ()) ind, Declareops.no_seff)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 31a96e6dce..72412d12dc 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -23,7 +23,8 @@ val rew_r2l_dep_scheme_kind : individual scheme_kind
 val rew_r2l_scheme_kind : individual scheme_kind
 
 val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
-val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
+val build_l2r_rew_scheme :
+  bool -> env -> inductive -> sorts_family -> constr * Declareops.side_effects
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> sorts_family -> constr
 val build_l2r_forward_rew_scheme :
@@ -34,7 +35,8 @@ val build_l2r_forward_rew_scheme :
 val build_sym_scheme : env -> inductive -> constr
 val sym_scheme_kind : individual scheme_kind
 
-val build_sym_involutive_scheme : env -> inductive -> constr
+val build_sym_involutive_scheme :
+  env -> inductive -> constr * Declareops.side_effects
 val sym_involutive_scheme_kind : individual scheme_kind
 
 (** Builds a congruence scheme for an equality type *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b991defe73..f5ab039b42 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -283,12 +283,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	  begin 
 	    try 
 	      let _ = Global.lookup_constant c1' in
-	      mkConst c1'
+              mkConst c1', gl
 	    with Not_found -> 
 	      let rwr_thm = Label.to_string l' in 
 	      error ("Cannot find rewrite principle "^rwr_thm^".")
 	  end
-	| _ -> pr1
+	| _ -> pr1, gl
         end
       | _ -> 
 	  (* cannot occur since we checked that we are in presence of 
@@ -308,7 +308,10 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
     | true, _, false -> rew_r2l_forward_dep_scheme_kind
   in
   match kind_of_term hdcncl with
-  | Ind ind -> mkConst (find_scheme scheme_name ind)
+  | Ind ind -> 
+      let c, eff = find_scheme scheme_name ind in 
+      let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
+      mkConst c, gl
   | _ -> assert false
 
 let type_of_clause gl = function
@@ -319,7 +322,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze
   let isatomic = isProd (whd_zeta hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
-  let elim = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+  let elim, gl = find_elim hdcncl lft2rgt dep cls (Some t) gl in
   general_elim_clause with_evars frzevars tac cls sigma c t l
     (match lft2rgt with None -> false | Some b -> b)
     {elimindex = None; elimbody = (elim,NoBindings)} gl
@@ -775,14 +778,16 @@ let ind_scheme_of_eq lbeq =
   let kind =
     if kind == InProp then Elimschemes.ind_scheme_kind_from_prop
     else Elimschemes.ind_scheme_kind_from_type in
-  mkConst (find_scheme kind (destInd lbeq.eq))
+  let c, eff = find_scheme kind (destInd lbeq.eq) in
+  mkConst c, eff
 
 
 let discrimination_pf e (t,t1,t2) discriminator lbeq =
-  let i           = build_coq_I () in
-  let absurd_term = build_coq_False () in
-  let eq_elim     = ind_scheme_of_eq lbeq in
-  (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term)
+  let i            = build_coq_I () in
+  let absurd_term  = build_coq_False () in
+  let eq_elim, eff = ind_scheme_of_eq lbeq in
+  (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
+  eff
 
 let eq_baseid = Id.of_string "e"
 
@@ -795,17 +800,19 @@ let apply_on_clause (f,t) clause =
      | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
   clenv_fchain argmv f_clause clause
 
-let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
+let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl=
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
   let discriminator =
     build_discriminator sigma e_env dirn (mkVar e) sort cpath in
-  let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
+  let (pf, absurd_term), eff =
+    discrimination_pf e (t,t1,t2) discriminator lbeq in
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = clenv_value_cast_meta absurd_clause in
+  let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
   tclTHENS (cut_intro absurd_term)
-    [onLastHypId gen_absurdity; refine pf]
+    [onLastHypId gen_absurdity; refine pf] gl
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls =
   let sigma = eq_clause.evd in
@@ -1134,7 +1141,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
 
-let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
+let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl =
   (* fetch the informations of the  pair *)
   let ceq = constr_of_global Coqlib.glob_eq in
   let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
@@ -1153,19 +1160,19 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
     Library.require_library [Loc.ghost,eqdep_dec] (Some false);
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
+    let gl = { gl with eff = Declareops.union_side_effects eff gl.eff } in
       (* cut with the good equality and prove the requested goal *)
     tclTHENS (cut (mkApp (ceq,new_eq_args)))
       [tclIDTAC; tclTHEN (apply (
-        mkApp(inj2,
-              [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
-                ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
+        mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
        )) (Auto.trivial [] [])
-      ]
+      ] gl
   (* not a dep eq or no decidable type found *)
   end
   else raise Not_dep_pair
 
-let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause gl =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
@@ -1178,10 +1185,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
     | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
         errorlabstrm "Equality.inj" (str"Nothing to inject.")
     | Inr posns ->
-        try inject_if_homogenous_dependent_pair env sigma u
+        try inject_if_homogenous_dependent_pair env sigma u gl
         with e when (Errors.noncritical e || e = Not_dep_pair) ->
         inject_at_positions env sigma l2r u eq_clause posns
-          (tac (clenv_value eq_clause))
+          (tac (clenv_value eq_clause)) gl
 
 let postInjEqTac ipats c n =
   match ipats with
@@ -1255,7 +1262,7 @@ let swapEquandsInConcl gls =
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim lbeq.eq (Some false) false None None gls in
+  let eq_elim, gls = find_elim lbeq.eq (Some false) false None None gls in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e14c234213..ae617a4d8a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -115,7 +115,8 @@ TACTIC EXTEND ediscriminate
 END
 
 let discrHyp id gl =
-  discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl
+  discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
+              eff = gl.eff} gl
 
 let injection_main c =
  elimOnConstrWithHoles (injClause None) false c
@@ -159,7 +160,8 @@ TACTIC EXTEND einjection_as
 END
 
 let injHyp id gl =
-  injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl
+  injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
+                   eff = gl.eff } gl
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -765,6 +767,6 @@ END;;
    mode. *)
 VERNAC COMMAND EXTEND GrabEvars
 [ "Grab" "Existential" "Variables" ] ->
-  [ let p = Proof_global.give_me_the_proof () in
-    Proof.V82.grab_evars p ]
+  [ Proof_global.with_current_proof (fun _ p  ->
+      Proof.V82.grab_evars p) ]
 END
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index ac4cd54423..63a5917771 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -196,7 +196,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     (str"Computed inversion goal was not closed in initial signature.");
   *)
   let pf = Proof.start [invEnv,invGoal] in
-  Proof.run_tactic env (Proofview.V82.tactic (tclTHEN intro (onLastHypId inv_op))) pf;
+  let pf = Proof.run_tactic env 
+    (Proofview.V82.tactic (tclTHEN intro (onLastHypId inv_op))) pf in
   let pfterm = List.hd (Proof.partial_proof pf) in
   let global_named_context = Global.named_context () in
   let ownSign = ref begin
@@ -227,7 +228,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof = inversion_scheme env sigma t sort dep inv_op in
   let entry = {
-    const_entry_body = invProof;
+    const_entry_body = Future.from_val (invProof,Declareops.no_seff);
     const_entry_secctx = None;
     const_entry_type = None;
     const_entry_opaque = false;
@@ -241,8 +242,8 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 
 let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op =
   let pts = get_pftreestate() in
-  let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in
-  let gl = { it = List.nth gls (n-1) ; sigma=sigma } in
+  let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
+  let gl = { it = List.nth gls (n-1) ; sigma=sigma; eff=eff } in
   let t =
     try pf_get_hyp_typ gl id
     with Not_found -> Pretype_errors.error_var_not_found_loc loc id in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c88e67e8b0..154cad6913 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -683,7 +683,7 @@ let reset_env env =
 let fold_match ?(force=false) env sigma c =
   let (ci, p, c, brs) = destCase c in
   let cty = Retyping.get_type_of env sigma c in
-  let dep, pred, exists, sk = 
+  let dep, pred, exists, (sk, eff) = 
     let env', ctx, body =
       let ctx, pred = decompose_lam_assum p in
       let env' = Environ.push_rel_context ctx env in
@@ -720,7 +720,7 @@ let fold_match ?(force=false) env sigma c =
     let meths = List.map (fun br -> br) (Array.to_list brs) in
       applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
   in 
-    sk, (if exists then env else reset_env env), app
+    sk, (if exists then env else reset_env env), app, eff
       
 let unfold_match env sigma sk app =
   match kind_of_term app with
@@ -897,7 +897,7 @@ let subterm all flags (s : strategy) : strategy =
 	      else
 		match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
 		| None -> x
-		| Some (cst, _, t') ->
+		| Some (cst, _, t',_) -> (* eff XXX *)
 		  match aux env avoid t' ty cstr evars with
 		  | Some (Some prf) -> 
 		    Some (Some { prf with
@@ -1251,7 +1251,9 @@ let assert_replacing id newt tac =
 			  env ~init:[]
 		      in
 		      let (e, args) = destEvar ev in
-			Goal.return (mkEvar (e, Array.of_list inst)))))
+			Goal.return 
+                         (mkEvar (e, Array.of_list inst))
+                         Declareops.no_seff)))
        in Goal.bind reft Goal.refine)
   in Proofview.tclTHEN (Proofview.tclSENSITIVE sens) 
        (Proofview.tclFOCUS 2 2 tac)
@@ -1295,7 +1297,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	   try 
 	     let res = 
 	       cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp 
-	     in return (res, is_hyp)
+	     in return (res, is_hyp) Declareops.no_seff
 	   with
 	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	     raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
@@ -1316,9 +1318,9 @@ let cl_rewrite_clause_new_strat ?abs strat clause =
    newfail 0 (str"setoid rewrite failed: " ++ s))
 
 let cl_rewrite_clause_newtac' l left2right occs clause =
-  Proof_global.run_tactic 
+  Proof_global.with_current_proof (fun _ -> Proof.run_tactic (Global.env ())
     (Proofview.tclFOCUS 1 1 
-       (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause))
+       (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)))
 
 let cl_rewrite_clause_strat strat clause =
   tclTHEN (tactic_init_setoid ())
@@ -1722,7 +1724,8 @@ let declare_projection n instance_id r =
   let ty = Global.type_of_global r in
   let c = constr_of_global r in
   let term = proper_projection c ty in
-  let typ = Typing.type_of (Global.env ()) Evd.empty term in
+  let env = Global.env() in
+  let typ = Typing.type_of env Evd.empty term in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n =
@@ -1739,12 +1742,12 @@ let declare_projection n instance_id r =
 	  | _ -> typ
       in aux init
     in
-    let ctx,ccl = Reductionops.splay_prod_n (Global.env()) Evd.empty (3 * n) typ
+    let ctx,ccl = Reductionops.splay_prod_n env Evd.empty (3 * n) typ
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
   let cst =
-    { const_entry_body = term;
+    { const_entry_body = Future.from_val (term,Declareops.no_seff);
       const_entry_secctx = None;
       const_entry_type = Some typ;
       const_entry_opaque = false;
@@ -2052,26 +2055,30 @@ TACTIC EXTEND implify
 [ "implify" hyp(n) ] -> [ implify n ]
 END
 
-let rec fold_matches env sigma c =
+let rec fold_matches eff env sigma c =
   map_constr_with_full_binders Environ.push_rel 
     (fun env c ->
       match kind_of_term c with
       | Case _ ->
-          let cst, env, c' = fold_match ~force:true env sigma c in
-	    fold_matches env sigma c'
-      | _ -> fold_matches env sigma c)
+          let cst, env, c',eff' = fold_match ~force:true env sigma c in
+          eff := Declareops.union_side_effects eff' !eff;
+          fold_matches eff env sigma c'
+      | _ -> fold_matches eff env sigma c)
     env c
 
 TACTIC EXTEND fold_match
 [ "fold_match" constr(c) ] -> [ fun gl -> 
-  let _, _, c' = fold_match ~force:true (pf_env gl) (project gl) c in
-    change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
+  let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in
+   tclTHEN (Tactics.emit_side_effects eff)
+    (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl ]
 END
 
 TACTIC EXTEND fold_matches
-| [ "fold_matches" constr(c) ] -> [ fun gl -> 
-  let c' = fold_matches (pf_env gl) (project gl) c in
-    change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
+| [ "fold_matches" constr(c) ] -> [ fun gl ->
+  let eff = ref Declareops.no_seff in
+  let c' = fold_matches eff (pf_env gl) (project gl) c in
+  tclTHEN (Tactics.emit_side_effects !eff)
+    (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl ]
 END
 
 TACTIC EXTEND myapply
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1b460b060b..d8e03265d5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1046,7 +1046,7 @@ let mk_open_constr_value ist gl c =
 let mk_hyp_value ist gl c = Value.of_constr (mkVar (interp_hyp ist gl c))
 let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c)
 
-let pack_sigma (sigma,c) = {it=c;sigma=sigma}
+let pack_sigma eff (sigma,c) = {it=c;sigma=sigma;eff=eff}
 
 let extend_gl_hyps { it=gl ; sigma=sigma } sign =
   Goal.V82.new_goal_with sigma gl sign
@@ -1317,7 +1317,7 @@ and interp_letin ist gl llc u =
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist goal lz lr lmr =
   let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in
-  let goal = { it = gl ; sigma = sigma } in
+  let goal = { it = gl ; sigma = sigma; eff = sig_eff goal } in
   let hyps = pf_hyps goal in
   let hyps = if lr then List.rev hyps else hyps in
   let concl = pf_concl goal in
@@ -1457,11 +1457,11 @@ and interp_genarg ist gl x =
            (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
     | ConstrWithBindingsArgType ->
       in_gen (topwit wit_constr_with_bindings)
-        (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl)
+        (pack_sigma (sig_eff gl) (interp_constr_with_bindings ist (pf_env gl) (project gl)
 		       (out_gen (glbwit wit_constr_with_bindings) x)))
     | BindingsArgType ->
       in_gen (topwit wit_bindings)
-        (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
+        (pack_sigma (sig_eff gl) (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
     | ListArgType ConstrArgType ->
         let (sigma,v) = interp_genarg_constr_list ist gl x in
 	evdref := sigma;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 06ad729d44..ee92762cbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3594,6 +3594,9 @@ let abstract_subproof id tac gl =
   (** ppedrot: seems legit to have abstracted subproofs as local*)
   let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
   let lem = mkConst cst in
+  let gl = {gl with eff =
+    Declareops.cons_side_effects
+      (Safe_typing.sideff_of_con (Global.safe_env()) cst) gl.eff} in
   exact_no_check
     (applist (lem,List.rev (instance_from_named_context sign)))
     gl
@@ -3621,3 +3624,9 @@ let unify ?(state=full_transparent_state) x y gl =
     let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
     in tclEVARS evd gl
   with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
+
+let emit_side_effects eff gl = 
+  Declareops.iter_side_effects (fun e ->
+    prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e))
+    eff;
+  {gl with it = [gl.it] ; eff = Declareops.union_side_effects eff gl.eff}
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index cdc8eb3757..7acd803bd8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -398,7 +398,10 @@ val general_multi_rewrite :
 val subst_one :
   (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t
 
+
 val declare_intro_decomp_eq :
   ((int -> tactic) -> Coqlib.coq_eq_data * types *
    (types * constr * constr) ->
    clausenv -> tactic) -> unit
+
+val emit_side_effects : Declareops.side_effects -> tactic