From 26d180fa0b27edc773fd07c73906e4ed56475200 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 16 Nov 2016 10:51:39 +0100 Subject: [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. --- printing/ppvernac.ml | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'printing') 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") -- cgit v1.2.3