1 files changed, 47 insertions, 41 deletions

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 =