diff options
| author | Emilio Jesus Gallego Arias | 2016-11-16 10:51:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-11-17 10:14:40 +0100 |
| commit | 26d180fa0b27edc773fd07c73906e4ed56475200 (patch) | |
| tree | 7b79952cd7221013f444dfdf8b3b9732be8365a1 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9b52d1bf31..4ba9eeefa9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -64,16 +64,6 @@ GEXTEND Gram | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) - (* Stm backdoor *) - | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument - | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish - | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait - | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag - | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> - VernacStm (Observe (Stateid.of_int (int_of_string id))) - | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) - | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) - | v = vernac_poly -> v ] ] ; |