diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/logic.ml | 1 | ||||
-rw-r--r-- | proofs/pfedit.ml | 5 | ||||
-rw-r--r-- | proofs/proof.ml | 7 | ||||
-rw-r--r-- | proofs/proof.mli | 2 |
4 files changed, 8 insertions, 7 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 13a4e4ce3..a9ad606a0 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -11,7 +11,6 @@ open CErrors open Util open Names open Nameops -open Term open Constr open Vars open Termops 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 |