diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 8 |
1 files changed, 5 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} ; |