diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index ba4980b66b..413b5fdd7e 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -112,7 +112,7 @@ type proof = { (* List of goals that have been given up *) given_up : Goal.goal list; (* The initial universe context (for the statement) *) - initial_euctx : Evd.evar_universe_context + initial_euctx : UState.t } (*** General proof functions ***) @@ -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; } = |