aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml10
-rw-r--r--plugins/setoid_ring/newring.ml43
-rw-r--r--pretyping/evd.ml19
-rw-r--r--pretyping/evd.mli15
-rw-r--r--printing/printer.ml10
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--proofs/goal.ml91
-rw-r--r--proofs/goal.mli8
-rw-r--r--proofs/logic.ml10
-rw-r--r--proofs/pfedit.ml8
-rw-r--r--proofs/proof.ml8
-rw-r--r--proofs/proof.mli3
-rw-r--r--proofs/proof_global.ml13
-rw-r--r--proofs/proofview.ml67
-rw-r--r--proofs/proofview.mli2
-rw-r--r--proofs/refiner.ml54
-rw-r--r--proofs/refiner.mli8
-rw-r--r--proofs/tacmach.ml3
-rw-r--r--proofs/tacmach.mli10
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/class_tactics.ml40
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/extratactics.ml46
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/rewrite.ml23
-rw-r--r--tactics/tacinterp.ml8
-rw-r--r--tactics/tactics.ml9
-rw-r--r--toplevel/vernacentries.ml4
28 files changed, 225 insertions, 221 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index cca17a17e1..e18df6e460 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -51,13 +51,13 @@ let _ =
let tcl_change_info_gen info_gen =
(fun gls ->
- let it, eff = sig_it gls, sig_eff gls in
+ let it = sig_it gls in
let concl = pf_concl gls in
let hyps = Goal.V82.hyps (project gls) it in
let extra = Goal.V82.extra (project gls) it in
let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
let sigma = Goal.V82.partial_solution sigma it ev in
- { it = [gl] ; sigma= sigma; eff = eff } )
+ { it = [gl] ; sigma= sigma; } )
let tcl_change_info info gls =
let info_gen s = Store.set s Decl_mode.info info in
@@ -129,7 +129,7 @@ let go_to_proof_mode () =
let daimon_tac gls =
set_daimon_flag ();
- {it=[];sigma=sig_sig gls;eff=gls.eff}
+ {it=[];sigma=sig_sig gls;}
(* post-instruction focus management *)
@@ -1455,8 +1455,8 @@ let do_instr raw_instr pts =
let has_tactic = preprocess pts raw_instr.instr in
begin
if has_tactic then
- let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
- let gl = { it=List.hd gls ; sigma=sigma; eff=eff } in
+ let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
+ let gl = { it=List.hd gls ; sigma=sigma; } in
let env= pf_env gl in
let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
gsigma = sigma; genv = env} in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 30ceb10182..74ad34eff6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -179,8 +179,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
let dummy_goal env =
let (gl,_,sigma) =
Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
- {Evd.it = gl; Evd.eff=Declareops.no_seff;
- Evd.sigma = sigma}
+ {Evd.it = gl; Evd.sigma = sigma}
let exec_tactic env n f args =
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1aa8997710..84eba701ed 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -200,7 +200,8 @@ type evar_map = {
univ_cstrs : Univ.universes;
conv_pbs : evar_constraint list;
last_mods : Evar.Set.t;
- metas : clbinding Metamap.t
+ metas : clbinding Metamap.t;
+ effects : Declareops.side_effects;
}
(*** Lifting primitive from EvarMap. ***)
@@ -361,6 +362,7 @@ let empty = {
conv_pbs = [];
last_mods = Evar.Set.empty;
metas = Metamap.empty;
+ effects = Declareops.no_seff;
}
let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
@@ -463,6 +465,17 @@ let collect_evars c =
collrec Evar.Set.empty c
(**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+ { evd with effects = Declareops.union_side_effects eff evd.effects; }
+
+let drop_side_effects evd =
+ { evd with effects = Declareops.no_seff; }
+
+let eval_side_effects evd = evd.effects
+
+(**********************************************************)
(* Sort variables *)
let new_univ_variable evd =
@@ -659,15 +672,11 @@ type open_constr = evar_map * constr
type ['a] *)
type 'a sigma = {
it : 'a ;
- eff : Declareops.side_effects;
sigma : evar_map
}
let sig_it x = x.it
-let sig_eff x = x.eff
let sig_sig x = x.sigma
-let emit_side_effects eff x =
- { x with eff = Declareops.union_side_effects eff x.eff }
(**********************************************************)
(* Failure explanation *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a5ff11c7ed..5ef243e136 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -195,6 +195,17 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
(** Convenience function. Wrapper around {!find} to recover the source of an
evar in a given evar map. *)
+(** {5 Side-effects} *)
+
+val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
+(** Push a side-effect into the evar map. *)
+
+val eval_side_effects : evar_map -> Declareops.side_effects
+(** Return the effects contained in the evar map. *)
+
+val drop_side_effects : evar_map -> evar_map
+(** This should not be used. For hacking purposes. *)
+
(** {5 Sort variables}
Evar maps also keep track of the universe constraints defined at a given
@@ -212,8 +223,6 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
type 'a sigma = {
it : 'a ;
(** The base object. *)
- eff : Declareops.side_effects;
- (** Sideffects to be handled by the state machine. *)
sigma : evar_map
(** The added unification state. *)
}
@@ -221,9 +230,7 @@ type 'a sigma = {
['a]. *)
val sig_it : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
val sig_sig : 'a sigma -> evar_map
-val emit_side_effects : Declareops.side_effects -> 'a sigma -> 'a sigma
(** {5 Meta machinery}
diff --git a/printing/printer.ml b/printing/printer.ml
index 0e5d6721ed..2038fdeaa7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -388,7 +388,7 @@ let default_pr_subgoal n sigma =
| [] -> error "No such goal."
| g::rest ->
if Int.equal p 1 then
- let pg = default_pr_goal { sigma=sigma ; it=g; eff=Declareops.no_seff } in
+ let pg = default_pr_goal { sigma=sigma ; it=g; } in
v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
++ str " is:" ++ cut () ++ pg)
else
@@ -439,7 +439,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
in
let print_multiple_goals g l =
if pr_first then
- default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } ++
+ default_pr_goal { it = g ; sigma = sigma; } ++
pr_rec 2 l
else
pr_rec 1 (g::l)
@@ -464,13 +464,13 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
str "You can use Grab Existential Variables.")
end
| [g],[] when not !Flags.print_emacs ->
- let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
+ let pg = default_pr_goal { it = g ; sigma = sigma; } in
v 0 (
str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg
++ emacs_print_dependent_evars sigma seeds
)
| [g],a::l when not !Flags.print_emacs ->
- let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
+ let pg = default_pr_goal { it = g ; sigma = sigma; } in
v 0 (
str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg
++ emacs_print_dependent_evars sigma seeds
@@ -556,7 +556,7 @@ let pr_goal_by_id id =
++ pr_goal gs)
in
try
- Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;eff=Declareops.no_seff})
+ Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;})
with Not_found -> error "Invalid goal identifier."
(* Elementary tactics *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 4260d5553b..a79c9f9785 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -113,7 +113,7 @@ let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
let env = pf_env gls in
let evd = create_goal_evar_defs (project gls) in
let evd' = w_unify env evd CONV ~flags m n in
- tclIDTAC {it = gls.it; sigma = evd'; eff = gls.eff}
+ tclIDTAC {it = gls.it; sigma = evd'; }
let unify ?(flags=fail_quick_unif_flags) m gls =
let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 68eb1c5861..0eacde8780 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -87,8 +87,7 @@ type subgoals = { subgoals: goal list }
optimisation, since it will generaly not change during the
evaluation. *)
type 'a sensitive =
- Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info ->
- 'a * Declareops.side_effects
+ Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a
(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
(* the evar_info corresponding to the goal is computed at once
@@ -97,25 +96,24 @@ let eval t env defs gl =
let info = content defs gl in
let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
let rdefs = ref defs in
- let r, eff = t env rdefs gl info in
- ( r , !rdefs, eff )
+ let r = t env rdefs gl info in
+ ( r , !rdefs )
(* monadic bind on sensitive expressions *)
let bind e f env rdefs goal info =
- let a, eff1 = e env rdefs goal info in
- let b, eff2 = f a env rdefs goal info in
- b, Declareops.union_side_effects eff1 eff2
+ let a = e env rdefs goal info in
+ let b = f a env rdefs goal info in
+ b
(* monadic return on sensitive expressions *)
-let return v e _ _ _ _ = v, e
+let return v _ _ _ _ = v
(* interpretation of "open" constr *)
(* spiwack: it is a wrapper around [Constrintern.interp_open_constr].
In an ideal world, this could/should be the other way round.
As of now, though, it seems at least quite useful to build tactics. *)
let interp_constr cexpr env rdefs _ _ =
- let c = Constrintern.interp_constr_evars rdefs env cexpr in
- c, Declareops.no_seff
+ Constrintern.interp_constr_evars rdefs env cexpr
(* Type of constr with holes used by refine. *)
(* The list of evars doesn't necessarily contain all the evars in the constr,
@@ -135,18 +133,18 @@ module Refinable = struct
let make t env rdefs gl info =
let r = ref [] in
- let me, eff = t r env rdefs gl info in
- { me = me; my_evars = !r }, eff
+ let me = t r env rdefs gl info in
+ { me = me; my_evars = !r }
let make_with t env rdefs gl info =
let r = ref [] in
- let (me,side), eff = t r env rdefs gl info in
- ({ me = me ; my_evars = !r }, side), eff
+ let (me,side) = t r env rdefs gl info in
+ ({ me = me ; my_evars = !r }, side)
let mkEvar handle env typ _ rdefs _ _ =
let ev = Evarutil.e_new_evar rdefs env typ in
let (e,_) = destEvar ev in
handle := e::!handle;
- ev, Declareops.no_seff
+ ev
(* [with_type c typ] constrains term [c] to have type [typ]. *)
let with_type t typ env rdefs _ _ =
@@ -160,14 +158,13 @@ module Refinable = struct
Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ
in
rdefs := new_defs;
- j'.Environ.uj_val, Declareops.no_seff
+ j'.Environ.uj_val
(* spiwack: it is not very fine grain since it solves all typeclasses holes,
not only those containing the current goal, or a given term. But it
seems to fit our needs so far. *)
let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ =
- rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs;
- (), Declareops.no_seff
+ rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs
@@ -228,13 +225,13 @@ module Refinable = struct
Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc
in
ignore(update_handle handle init_defs !rdefs);
- open_constr, Declareops.no_seff
+ open_constr
let constr_of_open_constr handle check_type (evars, c) env rdefs gl info =
let delta = update_handle handle !rdefs evars in
rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
- else c, Declareops.no_seff
+ else c
end
@@ -255,7 +252,7 @@ let refine step env rdefs gl info =
let subgoals =
Option.List.flatten (List.map (advance !rdefs) subgoals)
in
- { subgoals = subgoals }, Declareops.no_seff
+ { subgoals = subgoals }
(*** Cleaning goals ***)
@@ -269,7 +266,7 @@ let clear ids env rdefs gl info =
let (cleared_evar,_) = destEvar cleared_concl in
let cleared_goal = descendent gl cleared_evar in
rdefs := Evd.define gl.content cleared_concl !rdefs;
- { subgoals = [cleared_goal] }, Declareops.no_seff
+ { subgoals = [cleared_goal] }
let wrap_apply_to_hyp_and_dependent_on sign id f g =
try Environ.apply_to_hyp_and_dependent_on sign id f g
@@ -325,27 +322,27 @@ let clear_body idents env rdefs gl info =
let (new_evar,_) = destEvar new_constr in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_constr defs';
- { subgoals = [new_goal] }, Declareops.no_seff
+ { subgoals = [new_goal] }
(*** Sensitive primitives ***)
(* [concl] is the conclusion of the current goal *)
let concl _ _ _ info =
- Evd.evar_concl info, Declareops.no_seff
+ Evd.evar_concl info
(* [hyps] is the [named_context_val] representing the hypotheses
of the current goal *)
let hyps _ _ _ info =
- Evd.evar_hyps info, Declareops.no_seff
+ Evd.evar_hyps info
(* [env] is the current [Environ.env] containing both the
environment in which the proof is ran, and the goal hypotheses *)
-let env env _ _ _ = env, Declareops.no_seff
+let env env _ _ _ = env
(* [defs] is the [Evd.evar_map] at the current evaluation point *)
let defs _ rdefs _ _ =
- !rdefs, Declareops.no_seff
+ !rdefs
(* Cf mli for more detailed comment.
[null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
@@ -363,7 +360,7 @@ let equal { content = e1 } { content = e2 } = Evar.equal e1 e2
let here goal value _ _ goal' _ =
if equal goal goal' then
- value, Declareops.no_seff
+ value
else
raise UndefinedHere
@@ -375,7 +372,7 @@ let rec list_mem_with eq x = function
let here_list goals value _ _ goal' _ =
if list_mem_with equal goal' goals then
- value, Declareops.no_seff
+ value
else
raise UndefinedHere
@@ -395,23 +392,23 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
d)
in
(* Modified named context. *)
- let new_hyps, effs1 =
- let hyps, effs = hyps env rdefs gl info in
- Environ.apply_to_hyp hyps id replace_function, effs
+ let new_hyps =
+ let hyps = hyps env rdefs gl info in
+ Environ.apply_to_hyp hyps id replace_function
in
let new_env = Environ.reset_with_named_context new_hyps env in
- let new_constr, effs2 =
- let concl, effs = concl env rdefs gl info in
- Evarutil.e_new_evar rdefs new_env concl, effs
+ let new_constr =
+ let concl = concl env rdefs gl info in
+ Evarutil.e_new_evar rdefs new_env concl
in
let (new_evar,_) = destEvar new_constr in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_constr !rdefs;
- { subgoals = [new_goal] }, Declareops.union_side_effects effs1 effs2
+ { subgoals = [new_goal] }
let convert_concl check cl' env rdefs gl info =
let sigma = !rdefs in
- let cl, effs = concl env rdefs gl info in
+ let cl = concl env rdefs gl info in
check_typability env sigma cl';
if (not check) || Reductionops.is_conv_leq env sigma cl' cl then
let new_constr =
@@ -420,7 +417,7 @@ let convert_concl check cl' env rdefs gl info =
let (new_evar,_) = destEvar new_constr in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_constr !rdefs;
- { subgoals = [new_goal] }, effs
+ { subgoals = [new_goal] }
else
Errors.error "convert-concl rule passed non-converting term"
@@ -433,20 +430,20 @@ let rename_hyp_sign id1 id2 sign =
(fun (_,b,t) _ -> (id2,b,t))
(fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
let rename_hyp id1 id2 env rdefs gl info =
- let hyps, effs1 = hyps env rdefs gl info in
+ let hyps = hyps env rdefs gl info in
if not (Names.Id.equal id1 id2) &&
List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
Errors.error ((Names.Id.to_string id2)^" is already used.");
let new_hyps = rename_hyp_sign id1 id2 hyps in
let new_env = Environ.reset_with_named_context new_hyps env in
- let old_concl, effs2 = concl env rdefs gl info in
+ let old_concl = concl env rdefs gl info in
let new_concl = Vars.replace_vars [id1,mkVar id2] old_concl in
let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
let new_subproof = Vars.replace_vars [id2,mkVar id1] new_subproof in
let (new_evar,_) = destEvar new_subproof in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_subproof !rdefs;
- { subgoals = [new_goal] }, Declareops.union_side_effects effs1 effs2
+ { subgoals = [new_goal] }
(*** Additional functions ***)
@@ -458,10 +455,10 @@ let rename_hyp id1 id2 env rdefs gl info =
*)
let rec list_map f l s =
match l with
- | [] -> ([],s,[])
- | a::l -> let (a,s,e) = f s a in
- let (l,s,es) = list_map f l s in
- (a::l,s,e::es)
+ | [] -> ([],s)
+ | a::l -> let (a,s) = f s a in
+ let (l,s) = list_map f l s in
+ (a::l,s)
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
@@ -525,7 +522,7 @@ module V82 = struct
to have functional content. *)
let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty evi in
- { Evd.it = build evk ; Evd.sigma = sigma; eff = Declareops.no_seff }
+ { Evd.it = build evk ; Evd.sigma = sigma; }
(* Makes a goal out of an evar *)
let build = build
@@ -567,7 +564,7 @@ module V82 = struct
{ evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
let new_evi = Typeclasses.mark_unresolvable new_evi in
let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
- { Evd.it = build evk ; sigma = new_sigma; eff = Declareops.no_seff }
+ { Evd.it = build evk ; sigma = new_sigma; }
(* Used by the compatibility layer and typeclasses *)
let nf_evar sigma gl =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 267d264931..c07c7f28ed 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -43,13 +43,13 @@ type +'a sensitive
(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
val eval :
'a sensitive -> Environ.env -> Evd.evar_map -> goal ->
- 'a * Evd.evar_map * Declareops.side_effects
+ 'a * Evd.evar_map
(* monadic bind on sensitive expressions *)
val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive
(* monadic return on sensitive expressions *)
-val return : 'a -> Declareops.side_effects -> 'a sensitive
+val return : 'a -> 'a sensitive
(* interpretation of "open" constr *)
@@ -171,9 +171,9 @@ val here_list : goal list -> 'a -> 'a sensitive
[Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
new evar_map to next definition *)
val list_map :
- (Evd.evar_map -> 'a -> 'b * Evd.evar_map * Declareops.side_effects) ->
+ (Evd.evar_map -> 'a -> 'b * Evd.evar_map) ->
'a list -> Evd.evar_map ->
- 'b list * Evd.evar_map * Declareops.side_effects list
+ 'b list * Evd.evar_map
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e93319cae8..f883317503 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -573,10 +573,10 @@ let prim_refiner r sigma goal =
Goal.list_map (fun sigma (_,_,c) ->
let gl,ev,sig' =
Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
- (gl,ev),sig',Declareops.no_seff)
+ (gl,ev),sig')
all sigma
in
- let (gls_evs,sigma,_) = mk_sign sign all in
+ let (gls_evs,sigma) = mk_sign sign all in
let (gls,evs) = List.split gls_evs in
let ids = List.map pi1 all in
let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
@@ -615,10 +615,10 @@ let prim_refiner r sigma goal =
Goal.list_map (fun sigma(_,c) ->
let gl,ev,sigma =
Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
- (gl,ev),sigma,Declareops.no_seff)
- all sigma
+ (gl,ev),sigma)
+ all sigma
in
- let (gls_evs,sigma,_) = mk_sign sign all in
+ let (gls_evs,sigma) = mk_sign sign all in
let (gls,evs) = List.split gls_evs in
let (ids,types) = List.split all in
let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a45fe179ae..a44b3bef3a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -62,15 +62,15 @@ let _ = Errors.register_handler begin function
end
let get_nth_V82_goal i =
let p = Proof_global.give_me_the_proof () in
- let { it=goals ; sigma = sigma; eff = eff } = Proof.V82.subgoals p in
+ let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
try
- { it=(List.nth goals (i-1)) ; sigma=sigma; eff = eff }
+ { it=(List.nth goals (i-1)) ; sigma=sigma; }
with Failure _ -> raise NoSuchGoal
let get_goal_context_gen i =
try
-let { it=goal ; sigma=sigma; eff=eff } = get_nth_V82_goal i in
-(sigma, Refiner.pf_env { it=goal ; sigma=sigma; eff=eff })
+let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in
+(sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
let get_goal_context i =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8ad2458afa..712845f584 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -234,7 +234,7 @@ let _ = Errors.register_handler begin function
| _ -> raise Errors.Unhandled
end
-let return p t =
+let return p =
if not (is_done p) then
raise UnfinishedProof
else if has_unresolved_evar p then
@@ -242,7 +242,7 @@ let return p t =
raise HasUnresolvedEvar
else
let p = unfocus end_of_stack_kind p () in
- Proofview.return p.proofview t
+ Proofview.return p.proofview
let initial_goals p = Proofview.initial_goals p.proofview
@@ -271,10 +271,10 @@ module V82 = struct
Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
let top_goal p =
- let { Evd.it=gls ; sigma=sigma; eff=eff } =
+ let { Evd.it=gls ; sigma=sigma; } =
Proofview.V82.top_goals p.proofview
in
- { Evd.it=List.hd gls ; sigma=sigma; eff=eff }
+ { Evd.it=List.hd gls ; sigma=sigma; }
let top_evars p =
Proofview.V82.top_evars p.proofview
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 70615e09e3..fa6007061b 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -61,8 +61,7 @@ val partial_proof : proof -> Term.constr list
Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
exception UnfinishedProof
exception HasUnresolvedEvar
-val return :
- proof -> Term.constr -> Term.constr * Declareops.side_effects
+val return : proof -> Evd.evar_map
(*** Focusing actions ***)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d773eeb43d..81bfcaccee 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -280,16 +280,21 @@ let close_proof ~now fpl =
let return_proof ~fix_exn =
let { proof } = cur_pstate () in
let initial_goals = Proof.initial_goals proof in
- List.map (fun (c, _) ->
- try Proof.return proof c with
+ let evd =
+ try Proof.return proof with
| Proof.UnfinishedProof ->
raise (fix_exn(Errors.UserError("last tactic before Qed",
str"Attempt to save an incomplete proof")))
| Proof.HasUnresolvedEvar ->
raise (fix_exn(Errors.UserError("last tactic before Qed",
str"Attempt to save a proof with existential " ++
- str"variables still non-instantiated"))))
- initial_goals
+ str"variables still non-instantiated")))
+ in
+ let eff = Evd.eval_side_effects evd in
+ (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+ side-effects... This may explain why one need to uniquize side-effects
+ thereafter... *)
+ List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals
let close_future_proof proof = close_proof ~now:false proof
let close_proof () =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9467d2d710..625ae74f12 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -27,7 +27,6 @@ type proofview = {
initial : (Term.constr * Term.types) list;
solution : Evd.evar_map;
comb : Goal.goal list;
- side_effects : Declareops.side_effects
}
let proofview p =
@@ -40,7 +39,6 @@ let init =
| [] -> { initial = [] ;
solution = Evd.empty ;
comb = [];
- side_effects = Declareops.no_seff
}
| (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
aux l
@@ -52,8 +50,7 @@ let init =
let gl = Goal.build e in
{ initial = (econstr,typ)::ret;
solution = new_defs ;
- comb = gl::comb;
- side_effects = Declareops.no_seff }
+ comb = gl::comb; }
in
fun l -> let v = aux l in
(* Marks all the goal unresolvable for typeclasses. *)
@@ -69,13 +66,15 @@ let finished = function
| _ -> false
(* Returns the current value of the proofview partial proofs. *)
-let return { solution=defs; side_effects=eff } c = Evarutil.nf_evar defs c, eff
+let return { solution=defs } = defs
+
+let return_constr { solution = defs } c = Evarutil.nf_evar defs c
let partial_proof pv =
- List.map fst (List.map (return pv) (List.map fst (initial_goals pv)))
+ List.map (return_constr pv) (List.map fst (initial_goals pv))
let emit_side_effects eff x =
- { x with side_effects = Declareops.union_side_effects eff x.side_effects }
+ { x with solution = Evd.emit_side_effects eff x.solution }
(* spiwack: this function should probably go in the Util section,
but I'd rather have Util (or a separate module for lists)
@@ -366,8 +365,8 @@ let rec catchable_exception = function
[s] to each goal successively and applying [k] to each result. *)
let list_of_sensitive s k env step =
Goal.list_map begin fun defs g ->
- let (a,defs,effs) = Goal.eval s env defs g in
- (k a) , defs, effs
+ let (a,defs) = Goal.eval s env defs g in
+ (k a) , defs
end step.comb step.solution
(* In form of a tactic *)
let list_of_sensitive s k env =
@@ -376,10 +375,8 @@ let list_of_sensitive s k env =
let (>>) = Inner.seq in
Inner.get >>= fun step ->
try
- let (tacs,defs,effs) = list_of_sensitive s k env step in
- Inner.set { step with solution = defs;
- side_effects = Declareops.union_side_effects step.side_effects
- (Declareops.flatten_side_effects effs) } >>
+ let (tacs,defs) = list_of_sensitive s k env step in
+ Inner.set { step with solution = defs; } >>
Inner.return tacs
with e when catchable_exception e ->
tclZERO e env
@@ -400,23 +397,20 @@ let tclGOALBINDU s k =
(* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
everything is done in one step. *)
let sensitive_on_proofview s env step =
- let wrap g ((defs, partial_list, partial_eff) as partial_res) =
+ let wrap g ((defs, partial_list) as partial_res) =
match Goal.advance defs g with
| None -> partial_res
| Some g ->
- let { Goal.subgoals = sg } , d', eff = Goal.eval s env defs g in
- (d', sg::partial_list, eff::partial_eff)
+ let { Goal.subgoals = sg } , d' = Goal.eval s env defs g in
+ (d', sg::partial_list)
in
- let ( new_defs , combed_subgoals, side_effects ) =
- List.fold_right wrap step.comb (step.solution,[],[])
+ let ( new_defs , combed_subgoals ) =
+ List.fold_right wrap step.comb (step.solution,[])
in
{ step with
solution = new_defs;
- comb = List.flatten combed_subgoals;
- side_effects =
- Declareops.union_side_effects
- (Declareops.flatten_side_effects side_effects) step.side_effects }
-let tclSENSITIVE s env =
+ comb = List.flatten combed_subgoals; }
+ let tclSENSITIVE s env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Inner.bind in
Inner.get >>= fun step ->
@@ -456,25 +450,18 @@ module V82 = struct
try
let tac evd gl =
let glsigma =
- tac { Evd.it = gl ; sigma = evd; eff = Declareops.no_seff } in
+ tac { Evd.it = gl ; sigma = evd; } in
let sigma = glsigma.Evd.sigma in
let g = glsigma.Evd.it in
- ( g, sigma, glsigma.Evd.eff )
+ ( g, sigma )
in
(* Old style tactics expect the goals normalized with respect to evars. *)
- let no_side_eff f x y =
- let a, b = f x y in a, b, Declareops.no_seff in
- let (initgoals,initevd, eff1) =
- Goal.list_map (no_side_eff Goal.V82.nf_evar) ps.comb ps.solution
+ let (initgoals,initevd) =
+ Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
in
- let (goalss,evd,eff2) = Goal.list_map tac initgoals initevd in
+ let (goalss,evd) = Goal.list_map tac initgoals initevd in
let sgs = List.flatten goalss in
- Inner.set { ps with solution=evd ; comb=sgs;
- side_effects =
- Declareops.union_side_effects ps.side_effects
- (Declareops.union_side_effects
- (Declareops.flatten_side_effects eff1)
- (Declareops.flatten_side_effects eff2)) }
+ Inner.set { ps with solution=evd ; comb=sgs; }
with e when catchable_exception e ->
tclZERO e env
@@ -495,12 +482,12 @@ module V82 = struct
(* Returns the open goals of the proofview together with the evar_map to
interprete them. *)
- let goals { comb = comb ; solution = solution; side_effects=eff } =
- { Evd.it = comb ; sigma = solution; eff=eff}
+ let goals { comb = comb ; solution = solution; } =
+ { Evd.it = comb ; sigma = solution }
- let top_goals { initial=initial ; solution=solution; side_effects=eff } =
+ let top_goals { initial=initial ; solution=solution; } =
let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
- { Evd.it = goals ; sigma=solution; eff=eff }
+ { Evd.it = goals ; sigma=solution; }
let top_evars { initial=initial } =
let evars_of_initial (c,_) =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 2869e75e10..135b7205f2 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -44,7 +44,7 @@ val init : (Environ.env * Term.types) list -> proofview
val finished : proofview -> bool
(* Returns the current value of the proofview partial proofs. *)
-val return : proofview -> constr -> constr * Declareops.side_effects
+val return : proofview -> Evd.evar_map
val partial_proof : proofview -> constr list
val initial_goals : proofview -> (constr * types) list
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 06e35284d4..66e251d55c 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -16,7 +16,6 @@ open Logic
let sig_it x = x.it
-let sig_eff x = x.eff
let project x = x.sigma
(* Getting env *)
@@ -26,7 +25,7 @@ let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)
let refiner pr goal_sigma =
let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
- { it = sgl; sigma = sigma'; eff = goal_sigma.eff }
+ { it = sgl; sigma = sigma'; }
let norm_evar_tac gl = refiner (Change_evars) gl
@@ -35,19 +34,18 @@ let norm_evar_tac gl = refiner (Change_evars) gl
(*********************)
-let unpackage glsig = (ref (glsig.sigma)), glsig.it, (ref (glsig.eff))
+let unpackage glsig = (ref (glsig.sigma)), glsig.it
-let repackage e r v = {it = v; sigma = !r; eff = !e}
+let repackage r v = {it = v; sigma = !r; }
-let apply_sig_tac eff r tac g =
+let apply_sig_tac r tac g =
check_for_interrupt (); (* Breakpoint *)
- let glsigma = tac (repackage eff r g) in
+ let glsigma = tac (repackage r g) in
r := glsigma.sigma;
- eff := glsigma.eff;
glsigma.it
(* [goal_goal_list : goal sigma -> goal list sigma] *)
-let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; eff=gls.eff}
+let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; }
(* forces propagation of evar constraints *)
let tclNORMEVAR = norm_evar_tac
@@ -71,32 +69,32 @@ let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
let start_tac gls =
- let sigr, g, eff = unpackage gls in
- (sigr, [g], eff)
+ let sigr, g = unpackage gls in
+ (sigr, [g])
-let finish_tac (sigr,gl,eff) = repackage eff sigr gl
+let finish_tac (sigr,gl) = repackage sigr gl
(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last
m subgoals, and [tac] on the others *)
-let thens3parts_tac tacfi tac tacli (sigr,gs,eff) =
+let thens3parts_tac tacfi tac tacli (sigr,gs) =
let nf = Array.length tacfi in
let nl = Array.length tacli in
let ng = List.length gs in
if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
let gll =
(List.map_i (fun i ->
- apply_sig_tac eff sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
+ apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
0 gs) in
- (sigr,List.flatten gll, eff)
+ (sigr,List.flatten gll)
(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
let thensf_tac taci tac = thens3parts_tac taci tac [||]
(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
-let thensi_tac tac (sigr,gs,eff) =
+let thensi_tac tac (sigr,gs) =
let gll =
- List.map_i (fun i -> apply_sig_tac eff sigr (tac i)) 1 gs in
- (sigr, List.flatten gll, eff)
+ List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
+ (sigr, List.flatten gll)
let then_tac tac = thensf_tac [||] tac
@@ -198,9 +196,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
:Proof_type.goal list Evd.sigma =
let oldhyps:Context.named_context = pf_hyps goal in
let rslt:Proof_type.goal list Evd.sigma = tac goal in
- let {it=gls;sigma=sigma;eff=eff} = rslt in
+ let { it = gls; sigma = sigma; } = rslt in
let hyps:Context.named_context list =
- List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; eff=eff}) gls in
+ List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
let newhyps =
List.map (fun hypl -> List.subtract hypl oldhyps) hyps in
let emacs_str s =
@@ -250,8 +248,8 @@ let tclORELSE_THEN t1 t2then t2else gls =
with
| None -> t2else gls
| Some sgl ->
- let sigr, gl, eff = unpackage sgl in
- finish_tac (then_tac t2then (sigr,gl,eff))
+ let sigr, gl = unpackage sgl in
+ finish_tac (then_tac t2then (sigr,gl))
(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
let tclTRY f = (tclORELSE0 f tclIDTAC)
@@ -356,24 +354,24 @@ let tclIDTAC_list gls = gls
(* first_goal : goal list sigma -> goal sigma *)
let first_goal gls =
- let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in
+ let gl = gls.it and sig_0 = gls.sigma in
if List.is_empty gl then error "first_goal";
- { it = List.hd gl; sigma = sig_0 ; eff = eff_0 }
+ { it = List.hd gl; sigma = sig_0; }
(* goal_goal_list : goal sigma -> goal list sigma *)
let goal_goal_list gls =
- let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in
- { it = [gl]; sigma = sig_0; eff = eff_0 }
+ let gl = gls.it and sig_0 = gls.sigma in
+ { it = [gl]; sigma = sig_0; }
(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
let apply_tac_list tac glls =
- let (sigr,lg,eff) = unpackage glls in
+ let (sigr,lg) = unpackage glls in
match lg with
| (g1::rest) ->
- let gl = apply_sig_tac eff sigr tac g1 in
- repackage eff sigr (gl@rest)
+ let gl = apply_sig_tac sigr tac g1 in
+ repackage sigr (gl@rest)
| _ -> error "apply_tac_list"
let then_tactic_list tacl1 tacl2 glls =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index b2e753ea33..c198958e3d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -16,17 +16,15 @@ open Logic
(** The refiner (handles primitive rules and high-level tactics). *)
val sig_it : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
val project : 'a sigma -> evar_map
val pf_env : goal sigma -> Environ.env
val pf_hyps : goal sigma -> named_context
-val unpackage : 'a sigma -> evar_map ref * 'a * Declareops.side_effects ref
-val repackage : Declareops.side_effects ref -> evar_map ref -> 'a -> 'a sigma
+val unpackage : 'a sigma -> evar_map ref * 'a
+val repackage : evar_map ref -> 'a -> 'a sigma
val apply_sig_tac :
- Declareops.side_effects ref -> evar_map ref ->
- (goal sigma -> goal list sigma) -> goal -> goal list
+ evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
val refiner : rule -> tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fad46c99ba..84553e9ebc 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -22,7 +22,7 @@ open Proof_type
open Logic
open Refiner
-let re_sig it eff gc = { it = it; sigma = gc; eff = eff }
+let re_sig it gc = { it = it; sigma = gc; }
(**************************************************************)
(* Operations for handling terms under a local typing context *)
@@ -36,7 +36,6 @@ let repackage = Refiner.repackage
let apply_sig_tac = Refiner.apply_sig_tac
let sig_it = Refiner.sig_it
-let sig_eff = Refiner.sig_eff
let project = Refiner.project
let pf_env = Refiner.pf_env
let pf_hyps = Refiner.pf_hyps
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 19eb9ba7c0..ab59c64416 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -27,16 +27,14 @@ type 'a sigma = 'a Evd.sigma;;
type tactic = Proof_type.tactic;;
val sig_it : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
val project : goal sigma -> evar_map
-val re_sig : 'a -> Declareops.side_effects -> evar_map -> 'a sigma
+val re_sig : 'a -> evar_map -> 'a sigma
-val unpackage : 'a sigma -> evar_map ref * 'a * Declareops.side_effects ref
-val repackage : Declareops.side_effects ref -> evar_map ref -> 'a -> 'a sigma
+val unpackage : 'a sigma -> evar_map ref * 'a
+val repackage : evar_map ref -> 'a -> 'a sigma
val apply_sig_tac :
- Declareops.side_effects ref -> evar_map ref ->
- (goal sigma -> (goal list) sigma) -> goal -> (goal list)
+ evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6ed05d6b35..373a0bb62e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -972,7 +972,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; eff = Declareops.no_seff } in
+ let gl = { Evd.it = g; sigma = glss.Evd.sigma; } in
pr_hint_term (pf_concl gl)
(* displays the whole hint database db *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d80b7d738a..da6e123121 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -285,8 +285,8 @@ 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;eff=eff} ->
- let res = try Some (tac {it=gl; sigma=s;eff=eff})
+ { 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
match res with
| Some gls -> sk (f gls hints) fk
@@ -294,7 +294,7 @@ let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : '
let intro_tac : atac =
lift_tactic Tactics.intro
- (fun {it = gls; sigma = s;eff=eff} info ->
+ (fun {it = gls; sigma = s;} info ->
let gls' =
List.map (fun g' ->
let env = Goal.V82.env s g' in
@@ -303,13 +303,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;eff=eff})
+ in {it = gls'; sigma = s;})
let normevars_tac : atac =
- { skft = fun sk fk {it = (gl, info); sigma = s; eff=eff} ->
+ { skft = fun sk fk {it = (gl, info); sigma = s;} ->
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';eff=eff} fk }
+ sk {it = [gl', info']; sigma = sigma';} fk }
(* Ordering of states is lexicographic on the number of remaining goals. *)
let compare (pri, _, _, res) (pri', _, _, res') =
@@ -324,9 +324,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;eff=eff} ->
+ { skft = fun sk fk {it = gl,info; sigma = s;} ->
let concl = Goal.V82.concl s gl in
- let tacgl = {it = gl; sigma = s;eff=eff} in
+ let tacgl = {it = gl; sigma = s;} in
let poss = e_possible_resolve hints info.hints concl in
let rec aux i foundone = function
| (tac, _, b, name, pp) :: tl ->
@@ -338,7 +338,7 @@ let hints_tac hints =
in
(match res with
| None -> aux i foundone tl
- | Some {it = gls; sigma = s';eff=eff} ->
+ | Some {it = gls; sigma = s';} ->
if !typeclasses_debug then
msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
++ str" on" ++ spc () ++ pr_ev s gl);
@@ -370,11 +370,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';eff=eff}
+ ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';}
else info.hints;
auto_cut = derivs }
in g, info) 1 newgls in
- let glsv = {it = gls'; sigma = s';eff=eff} in
+ let glsv = {it = gls'; sigma = s';} in
sk glsv fk)
| [] ->
if not foundone && !typeclasses_debug then
@@ -417,14 +417,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; eff = Declareops.no_seff })
+ fk {it = (gl,info); sigma = s; })
| [] -> Somek2 (List.rev acc, s, fk)
- in fun {it = gls; sigma = s; eff = eff} fk ->
+ in fun {it = gls; sigma = s; } fk ->
let rec aux' = function
| Nonek2 -> fk ()
| Somek2 (res, s', fk') ->
let goals' = List.concat res in
- sk {it = goals'; sigma = s'; eff = eff } (fun () -> aux' (fk' ()))
+ sk {it = goals'; sigma = s'; } (fun () -> aux' (fk' ()))
in aux' (aux s [] (fun () -> Nonek2) gls)
let then_tac (first : atac) (second : atac) : atac =
@@ -463,8 +463,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'; eff = Declareops.no_seff } in
- (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; eff = Declareops.no_seff }
+ 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 get_result r =
match r with
@@ -489,11 +489,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; eff=g.eff } in
+ let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; } in
match run_tac (eauto_tac ?limit hints) gl with
| None -> raise Not_found
- | Some {it = goals; sigma = s; eff=eff} ->
- {it = List.map fst goals; sigma = s; eff=eff}
+ | Some {it = goals; sigma = s; } ->
+ {it = List.map fst goals; sigma = s;}
let real_eauto st ?limit hints p evd =
let rec aux evd fails =
@@ -539,7 +539,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; eff= Declareops.no_seff } in (* XXX eff *)
+ let gls = { it = gl ; sigma = sigma; } in
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/equality.ml b/tactics/equality.ml
index 1e01f47cd5..f5af80b0d5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -309,7 +309,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
match kind_of_term hdcncl with
| Ind ind ->
let c, eff = find_scheme scheme_name ind in
- let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
+ let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
mkConst c, gl
| _ -> assert false
@@ -809,7 +809,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl=
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
+ let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
tclTHENS (cut_intro absurd_term)
[onLastHypId gen_absurdity; refine pf] gl
@@ -1160,7 +1160,7 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl =
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
+ let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in
(* cut with the good equality and prove the requested goal *)
tclTHENS (cut (mkApp (ceq,new_eq_args)))
[tclIDTAC; tclTHEN (apply (
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a935f69002..32affcbe75 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -115,8 +115,7 @@ TACTIC EXTEND ediscriminate
END
let discrHyp id gl =
- discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
- eff = gl.eff} gl
+ discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;} gl
let injection_main c =
elimOnConstrWithHoles (injClause None) false c
@@ -160,8 +159,7 @@ TACTIC EXTEND einjection_as
END
let injHyp id gl =
- injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
- eff = gl.eff } gl
+ injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl; } gl
TACTIC EXTEND dependent_rewrite
| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 63a5917771..2a2a1e3560 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -242,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; eff=eff } = Proof.V82.subgoals pts in
- let gl = { it = List.nth gls (n-1) ; sigma=sigma; eff=eff } in
+ let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
+ let gl = { it = List.nth gls (n-1) ; sigma=sigma; } 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.ml b/tactics/rewrite.ml
index 7d3d5da612..fafafd8534 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1189,6 +1189,15 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
| Some None -> Some None
| None -> None
+(** ppedrot: this is a workaround. The current implementation of rewrite leaks
+ evar maps. We know that we should not produce effects in here, so we reput
+ them after computing... *)
+let tclEFFECT (tac : tactic) : tactic = fun gl ->
+ let eff = Evd.eval_side_effects gl.sigma in
+ let gls = tac gl in
+ let sigma = Evd.emit_side_effects eff (Evd.drop_side_effects gls.sigma) in
+ { gls with sigma; }
+
let cl_rewrite_clause_tac ?abs strat clause gl =
let evartac evd = Refiner.tclEVARS evd in
let treat res =
@@ -1227,7 +1236,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
Refiner.tclFAIL 0
(str"Unable to satisfy the rewriting constraints."
++ fnl () ++ Himsg.explain_typeclass_error env e)
- in tac gl
+ in tclEFFECT tac gl
let bind_gl_info f =
@@ -1266,8 +1275,7 @@ let assert_replacing id newt tac =
in
let (e, args) = destEvar ev in
Goal.return
- (mkEvar (e, Array.of_list inst))
- Declareops.no_seff)))
+ (mkEvar (e, Array.of_list inst)))))
in Goal.bind reft Goal.refine)
in Proofview.tclTHEN (Proofview.tclSENSITIVE sens)
(Proofview.tclFOCUS 2 2 tac)
@@ -1311,12 +1319,13 @@ 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) Declareops.no_seff
+ in return (res, is_hyp)
with
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
++ fnl () ++ Himsg.explain_typeclass_error env e)))
- in Proofview.tclGOALBINDU info (fun i -> treat i)
+ in
+ Proofview.tclGOALBINDU info (fun i -> treat i)
let newtactic_init_setoid () =
try init_setoid (); Proofview.tclUNIT ()
@@ -1726,10 +1735,10 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
(), res
in
try
- tclWEAK_PROGRESS
+ (tclWEAK_PROGRESS
(tclTHEN
(Refiner.tclEVARS hypinfo.cl.evd)
- (cl_rewrite_clause_tac ~abs:hypinfo.abs strat cl)) gl
+ (cl_rewrite_clause_tac ~abs:hypinfo.abs strat cl))) gl
with RewriteFailure e ->
let {l2r=l2r; c1=x; c2=y} = hypinfo in
raise (Pretype_errors.PretypeError
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 63d77af662..2a00f7defd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1045,7 +1045,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 eff (sigma,c) = {it=c;sigma=sigma;eff=eff}
+let pack_sigma (sigma,c) = {it=c;sigma=sigma;}
let extend_gl_hyps { it=gl ; sigma=sigma } sign =
Goal.V82.new_goal_with sigma gl sign
@@ -1316,7 +1316,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; eff = sig_eff goal } in
+ let goal = { it = gl ; sigma = sigma; } in
let hyps = pf_hyps goal in
let hyps = if lr then List.rev hyps else hyps in
let concl = pf_concl goal in
@@ -1456,11 +1456,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 (sig_eff gl) (interp_constr_with_bindings ist (pf_env gl) (project gl)
+ (pack_sigma (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 (sig_eff gl) (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
+ (pack_sigma (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 81ee6f19a0..298d26915f 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; }
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cd248e4cc3..8abac272c0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -93,8 +93,8 @@ let try_print_subgoals () =
let show_intro all =
let pf = get_pftreestate() in
- let {Evd.it=gls ; sigma=sigma; eff=eff} = Proof.V82.subgoals pf in
- let gl = {Evd.it=List.hd gls ; sigma = sigma; eff=eff} in
+ let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+ let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
if all
then
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:29:12 +0000