aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-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
14 files changed, 134 insertions, 153 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 08:46:52 +0000