diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 22c89cee69..12508d754e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1345,12 +1345,6 @@ let vernac_restart () = restart_proof(); print_subgoals () (* Proof switching *) -let vernac_suspend = suspend_proof - -let vernac_resume = function - | None -> resume_last_proof () - | Some id -> resume_proof id - let vernac_undo n = undo n; print_subgoals () @@ -1554,8 +1548,6 @@ let interp c = match c with | VernacAbort id -> vernac_abort id | VernacAbortAll -> vernac_abort_all () | VernacRestart -> vernac_restart () - | VernacSuspend -> vernac_suspend () - | VernacResume id -> vernac_resume id | VernacUndo n -> vernac_undo n | VernacUndoTo n -> undo_todepth n | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts |