aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli7
-rw-r--r--engine/proofview.mli1
-rw-r--r--ide/ide_slave.ml4
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/pfedit.ml5
-rw-r--r--proofs/proof.ml7
-rw-r--r--proofs/proof.mli2
-rw-r--r--tactics/hints.ml6
-rw-r--r--tactics/leminv.ml2
-rw-r--r--vernac/vernacentries.ml10
11 files changed, 29 insertions, 21 deletions
diff --git a/API/API.mli b/API/API.mli
index 8a4a6cc89..cc0de2b1b 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4645,16 +4645,23 @@ sig
type proof
type 'a focus_kind
+ val proof : proof ->
+ Goal.goal list * (Goal.goal list * Goal.goal list) list *
+ Goal.goal list * Goal.goal list * Evd.evar_map
+
val run_tactic : Environ.env ->
unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree)
val unshelve : proof -> proof
val maximal_unfocus : 'a focus_kind -> proof -> proof
val pr_proof : proof -> Pp.t
+
module V82 :
sig
val grab_evars : proof -> proof
val subgoals : proof -> Goal.goal list Evd.sigma
+ [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
+
end
end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0379d4b49..7f7acf874 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -563,6 +563,7 @@ module V82 : sig
(* Returns the open goals of the proofview together with the evar_map to
interpret them. *)
val goals : proofview -> Evar.t list Evd.sigma
+ [@@ocaml.deprecated "Use [Proofview.proofview]"]
val top_goals : entry -> proofview -> Evar.t list Evd.sigma
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 7cbab56d4..cfc0e09a0 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -217,7 +217,7 @@ let evars () =
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
let pfts = Proof_global.give_me_the_proof () in
- let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
+ let all_goals, _, _, _, sigma = Proof.proof pfts in
let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
let el = List.map map_evar exl in
@@ -227,7 +227,7 @@ let evars () =
let hints () =
try
let pfts = Proof_global.give_me_the_proof () in
- let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
+ let all_goals, _, _, _, sigma = Proof.proof pfts in
match all_goals with
| [] -> None
| g :: _ ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2fdc3bc37..b8d41d539 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1225,8 +1225,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let get_current_subgoals_types () =
let p = Proof_global.give_me_the_proof () in
- let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
- sigma, List.map (Goal.V82.abstract_type sigma) sgs
+ let sgs,_,_,_,sigma = Proof.proof p in
+ sigma, List.map (Goal.V82.abstract_type sigma) sgs
exception EmptySubgoals
let build_and_l sigma l =
diff --git a/printing/printer.ml b/printing/printer.ml
index 075b03b7d..ba31b72d6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -828,7 +828,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
let pr_nth_open_subgoal n =
let pf = Proof_global.give_me_the_proof () in
- let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+ let gls,_,_,_,sigma = Proof.proof pf in
pr_subgoal n sigma gls
let pr_goal_by_id id =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2d4aba17c..c526ae000 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -51,9 +51,8 @@ end
let get_nth_V82_goal i =
let p = Proof_global.give_me_the_proof () in
- let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
- try
- { it=(List.nth goals (i-1)) ; sigma=sigma; }
+ let goals,_,_,_,sigma = Proof.proof p in
+ try { it = List.nth goals (i-1) ; sigma }
with Failure _ -> raise NoSuchGoal
let get_goal_context_gen i =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e24d57f08..413b5fdd7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -163,6 +163,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals =
let rec unroll_focus pv = function
| (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
| [] -> pv
+
(* spiwack: a proof is considered completed even if its still focused, if the focus
doesn't hide any goal.
Unfocusing is handled in {!return}. *)
@@ -391,10 +392,12 @@ let pr_proof p =
(*** Compatibility layer with <=v8.2 ***)
module V82 = struct
let subgoals p =
- Proofview.V82.goals p.proofview
+ let it, sigma = Proofview.proofview p.proofview in
+ Evd.{ it; sigma }
let background_subgoals p =
- Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
+ let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in
+ Evd.{ it; sigma }
let top_goal p =
let { Evd.it=gls ; sigma=sigma; } =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 48aed8225..5756d06b6 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -65,7 +65,6 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
(*** General proof functions ***)
-
val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
val dependent_start : Proofview.telescope -> proof
val initial_goals : proof -> (EConstr.constr * EConstr.types) list
@@ -187,6 +186,7 @@ val pr_proof : proof -> Pp.t
(*** Compatibility layer with <=v8.2 ***)
module V82 : sig
val subgoals : proof -> Goal.goal list Evd.sigma
+ [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
(* All the subgoals of the proof, including those which are not focused. *)
val background_subgoals : proof -> Goal.goal list Evd.sigma
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c7c53b393..99be1846c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1467,11 +1467,11 @@ let pr_hint_term sigma cl =
(* print all hints that apply to the concl of the current goal *)
let pr_applicable_hint () =
let pts = Proof_global.give_me_the_proof () in
- let glss = Proof.V82.subgoals pts in
- match glss.Evd.it with
+ let glss,_,_,_,sigma = Proof.proof pts in
+ match glss with
| [] -> CErrors.user_err Pp.(str "No focused goal.")
| g::_ ->
- pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
+ pr_hint_term sigma (Goal.V82.concl sigma g)
let pp_hint_mode = function
| ModeInput -> str"+"
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cc9d98f6f..62f3866de 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -215,7 +215,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
invEnv ~init:Context.Named.empty
end in
let avoid = ref Id.Set.empty in
- let { sigma=sigma } = Proof.V82.subgoals pf in
+ let _,_,_,_,sigma = Proof.proof pf in
let sigma = Evd.nf_constraints sigma in
let rec fill_holes c =
match EConstr.kind sigma c with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a71794f5e..c00b107cf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -62,14 +62,12 @@ let show_proof () =
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
let pfts = Proof_global.give_me_the_proof () in
- let gls = Proof.V82.subgoals pfts in
- let sigma = gls.Evd.sigma in
+ let gls,_,_,_,sigma = Proof.proof pfts in
Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma))
let show_universes () =
let pfts = Proof_global.give_me_the_proof () in
- let gls = Proof.V82.subgoals pfts in
- let sigma = gls.Evd.sigma in
+ let gls,_,_,_,sigma = Proof.proof pfts in
let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
@@ -78,7 +76,7 @@ let show_universes () =
let show_intro all =
let open EConstr in
let pf = Proof_global.give_me_the_proof() in
- let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+ let gls,_,_,_,sigma = Proof.proof pf in
if not (List.is_empty gls) then begin
let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
@@ -1601,7 +1599,7 @@ let vernac_global_check c =
let get_nth_goal n =
let pf = Proof_global.give_me_the_proof() in
- let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+ let gls,_,_,_,sigma = Proof.proof pf in
let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
gl
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 07:29:53 +0000