diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 8 | ||||
| -rw-r--r-- | proofs/proof.mli | 3 |
2 files changed, 8 insertions, 3 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 84b6c133c4..27a65da4c7 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -259,13 +259,13 @@ let save pr = push_undo (save_state pr) pr (* This function restores a state, presumably from the top of the undo stack. *) -let restore_state save pr = +let restore_state save pr = match save with | State save -> pr.state <- save | Effect undo -> undo () (* Interpretes the Undo command. *) -let undo pr = +let undo pr = (* On a single line, since the effects commute *) restore_state (pop_undo pr) pr @@ -362,8 +362,10 @@ let no_focused_goal p = let end_of_stack_kind = new_focus_kind () let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind +let unfocused = is_last_focus end_of_stack_kind + let start goals = - let pr = + let pr = { state = { proofview = Proofview.init goals ; focus_stack = [] ; intel = Store.empty} ; diff --git a/proofs/proof.mli b/proofs/proof.mli index ef402fe606..715b3341b6 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -114,6 +114,9 @@ exception CannotUnfocusThisWay is not met. *) val unfocus : 'a focus_kind -> proof -> unit +(* [unfocused p] returns [true] when [p] is fully unfocused. *) +val unfocused : proof -> bool + (* [get_at_focus k] gets the information stored at the closest focus point of kind [k]. Raises [NoSuchFocus] if there is no focus point of kind [k]. *) |