diff options
| author | letouzey | 2012-03-23 16:49:47 +0000 |
|---|---|---|
| committer | letouzey | 2012-03-23 16:49:47 +0000 |
| commit | 3d1124c0acc9a126624a4ea6e71116fa8959b06b (patch) | |
| tree | 34629bc296668a9ddb3e0744e60dcb9947e2f8d5 /parsing | |
| parent | d1085fdbd8b9f64ec8d3f2c49b143004ea86a5ed (diff) | |
Remove old proof-managment commands Suspend/Resume
There're not compatible with the current Backtrack mecanism used
both by ProofGeneral and CoqIDE.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 3 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
2 files changed, 0 insertions, 5 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 9abb8cd17d..3851619809 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -58,9 +58,6 @@ GEXTEND Gram | IDENT "Defined" -> VernacEndProof (Proved (false,None)) | IDENT "Defined"; id=identref -> VernacEndProof (Proved (false,Some (id,None))) - | IDENT "Suspend" -> VernacSuspend - | IDENT "Resume" -> VernacResume None - | IDENT "Resume"; id = identref -> VernacResume (Some id) | IDENT "Restart" -> VernacRestart | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b569d2fa6f..c4ffbfd152 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -442,11 +442,9 @@ let rec pr_vernac = function (* Proof management *) | VernacAbortAll -> str "Abort All" | VernacRestart -> str"Restart" - | VernacSuspend -> str"Suspend" | VernacUnfocus -> str"Unfocus" | VernacGoal c -> str"Goal" ++ pr_lconstrarg c | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id - | VernacResume id -> str"Resume" ++ pr_opt pr_lident id | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i | VernacBacktrack (i,j,k) -> |