From 65eec025bc0b581fae1af78f18d1a8666b76e69b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sat, 5 Oct 2013 17:44:45 +0000 Subject: Moving side effects into evar_map. There was no reason to keep another state out of one we were threading all the way along. This should be safer, as one cannot forego side effects accidentally by manipulating explicitly the [sigma] container. Still, this patch raised the issue of badly used evar maps. There is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the fact it uses evar maps in an unorthodox way. Likewise, that mean we have to revert all contrib patches that added effect threading... There was also a dubious use of side effects in their toplevel handling, that duplicates them, leading to the need of a rather unsafe List.uniquize afterwards. It should be investigaged. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 81ee6f19a..298d26915 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3594,9 +3594,10 @@ let abstract_subproof id tac gl = (** ppedrot: seems legit to have abstracted subproofs as local*) let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in let lem = mkConst cst in - let gl = {gl with eff = - Declareops.cons_side_effects - (Safe_typing.sideff_of_con (Global.safe_env()) cst) gl.eff} in + let open Declareops in + let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in + let effs = cons_side_effects eff no_seff in + let gl = { gl with sigma = Evd.emit_side_effects effs gl.sigma; } in exact_no_check (applist (lem,List.rev (instance_from_named_context sign))) gl @@ -3629,4 +3630,4 @@ let emit_side_effects eff gl = Declareops.iter_side_effects (fun e -> prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e)) eff; - {gl with it = [gl.it] ; eff = Declareops.union_side_effects eff gl.eff} + { it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; } -- cgit v1.2.3