aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--proofs/pfedit.ml4
-rw-r--r--proofs/proof.ml8
-rw-r--r--proofs/proof.mli2
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--stm/stm.ml7
-rw-r--r--tactics/leminv.ml5
-rw-r--r--user-contrib/Ltac2/tac2entries.ml7
-rw-r--r--vernac/lemmas.ml6
9 files changed, 20 insertions, 26 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 4425e41652..4769c2dc53 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -102,6 +102,7 @@ let start_deriving f suchthat lemma =
let terminator = Proof_global.make_terminator terminator in
let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in
- fst @@ Proof_global.with_current_proof begin fun _ p ->
- Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
+ Proof_global.simple_with_current_proof begin fun _ p ->
+ let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
+ p
end pstate
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 4f36354f79..52e15f466f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -98,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
else tac
in
let env = Global.env () in
- let (p,(status,info)) = Proof.run_tactic env tac pr in
+ let (p,(status,info),()) = Proof.run_tactic env tac pr in
let env = Global.env () in
let sigma = Evd.from_env env in
let () =
@@ -161,7 +161,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
let prev_future_goals = save_future_goals sigma in
(* Start a proof *)
let prf = Proof.start ~name ~poly sigma [env, ty] in
- let (prf, _) =
+ let (prf, _, ()) =
try Proof.run_tactic env tac prf
with Logic_monad.TacticFailure e as src ->
(* Catch the inner error of the monad tactic *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 778d98b2cd..ce7354aa62 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -372,7 +372,7 @@ let run_tactic env tac pr =
let sp = pr.proofview in
let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
let tac =
- tac >>= fun () ->
+ tac >>= fun result ->
Proofview.tclEVARMAP >>= fun sigma ->
(* Already solved goals are not to be counted as shelved. Nor are
they to be marked as unresolvable. *)
@@ -383,10 +383,10 @@ let run_tactic env tac pr =
CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
- Proofview.tclUNIT retrieved
+ Proofview.tclUNIT (result,retrieved)
in
let { name; poly } = pr in
- let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
+ let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) =
Proofview.apply ~name ~poly env tac sp
in
let sigma = Proofview.return proofview in
@@ -400,7 +400,7 @@ let run_tactic env tac pr =
in
let given_up = pr.given_up@give_up in
let proofview = Proofview.Unsafe.reset_future_goals proofview in
- { pr with proofview ; shelf ; given_up },(status,info_trace)
+ { pr with proofview ; shelf ; given_up },(status,info_trace),result
(*** Commands ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1f4748141a..248b9d921e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -172,7 +172,7 @@ val no_focused_goal : t -> bool
used. In which case it is [false]. *)
val run_tactic
: Environ.env
- -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
+ -> 'a Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) * 'a
val maximal_unfocus : 'a focus_kind -> t -> t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 08b98d702a..40ae4acc88 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -345,6 +345,6 @@ let update_global_env (pf : t) =
with_current_proof (fun _ p ->
Proof.in_proof p (fun sigma ->
let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
- let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
+ let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in
(p, ()))) pf
in res
diff --git a/stm/stm.ml b/stm/stm.ml
index 3eb6d03529..21618bc044 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2085,8 +2085,8 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_fail ~st fail (fun () ->
(if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
- ignore(TaskQueue.with_n_workers nworkers (fun queue ->
- PG_compat.with_current_proof (fun _ p ->
+ TaskQueue.with_n_workers nworkers (fun queue ->
+ PG_compat.simple_with_current_proof (fun _ p ->
let Proof.{goals} = Proof.data p in
let open TacTask in
let res = CList.map_i (fun i g ->
@@ -2131,7 +2131,8 @@ end = struct (* {{{ *)
if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
end)
in
- Proof.run_tactic (Global.env()) assign_tac p)))) ())
+ let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in
+ p))) ())
end (* }}} *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 4aa4d13e1e..6efa1ece9c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
(str"Computed inversion goal was not closed in initial signature.");
*)
let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
- let pf =
- fst (Proof.run_tactic env (
- tclTHEN intro (onLastHypId inv_op)) pf)
- in
+ let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
let pfterm = List.hd (Proof.partial_proof pf) in
let global_named_context = Global.named_context_val () in
let ownSign = ref begin
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 9fd01426de..254c2e5086 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -740,7 +740,6 @@ let register_redefinition ?(local = false) qid e =
Lib.add_anonymous_leaf (inTac2Redefinition def)
let perform_eval ~pstate e =
- let open Proofview.Notations in
let env = Global.env () in
let (e, ty) = Tac2intern.intern ~strict:false e in
let v = Tac2interp.interp Tac2interp.empty_environment e in
@@ -761,12 +760,8 @@ let perform_eval ~pstate e =
| Goal_select.SelectAll -> v
| Goal_select.SelectAlreadyFocused -> assert false (* TODO **)
in
- (* HACK: the API doesn't allow to return a value *)
- let ans = ref None in
- let tac = (v >>= fun r -> ans := Some r; Proofview.tclUNIT ()) in
- let (proof, _) = Proof.run_tactic (Global.env ()) tac proof in
+ let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
let sigma = Proof.in_proof proof (fun sigma -> sigma) in
- let ans = match !ans with None -> assert false | Some r -> r in
let name = int_name () in
Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty)
++ spc () ++ str "=" ++ spc () ++
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1c7cc5e636..2dae0ad125 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -395,10 +395,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s
maybe_declare_manual_implicits false ref imps;
call_hook ?hook ctx [] strength ref) thms_data in
let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
- let pstate, _ = Proof_global.with_current_proof (fun _ p ->
+ let pstate = Proof_global.simple_with_current_proof (fun _ p ->
match init_tac with
- | None -> p,(true,[])
- | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in
+ | None -> p
+ | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
pstate
let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:35:58 +0000