diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-11-16 10:51:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-11-17 10:14:40 +0100 |
| commit | 26d180fa0b27edc773fd07c73906e4ed56475200 (patch) | |
| tree | 7b79952cd7221013f444dfdf8b3b9732be8365a1 /printing | |
| parent | 3a51aa7265f35dd3cbf3f7bff858d663e4406146 (diff) | |
[stm] Remove STM-related vernaculars
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3494ad006..a6b1c97f5 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -538,22 +538,6 @@ module Make | VernacLocal (local, v) -> return (pr_locality local ++ spc() ++ pr_vernac_body v) - (* 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 -> return (keyword "Abort All") |