diff options
| author | Emilio Jesus Gallego Arias | 2017-02-22 00:23:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-24 14:18:18 +0100 |
| commit | 584a832d4f681d34c7cbdd87d9ceb7a742b39959 (patch) | |
| tree | 1030c2c5a0a3dbfdb2b08773f2ca56ab80cde835 /printing | |
| parent | 530cd175c1b7465c3fa35c300f42b022bed9b25b (diff) | |
[stm] Remove some obsolete vernacs/classification.
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 78ef4d4bad..cfc2e48d11 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -534,18 +534,8 @@ open Decl_kinds (* Stm *) | VernacStm JoinDocument -> return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") | VernacStm Wait -> return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) (* Proof management *) | VernacAbortAll -> |