1 files changed, 8 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f4380c9d7..97b0ab51c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -76,6 +76,14 @@ GEXTEND Gram
       | IDENT "Fail"; v = vernac -> VernacFail v
       | IDENT "Local"; v = vernac_aux -> VernacLocal (true, v)
       | IDENT "Global"; v = vernac_aux -> VernacLocal (false, v)
+
+      (* Stm backdoor *)
+      | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
+      | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish
+      | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
+          VernacStm (Observe (Stateid.state_id_of_int (int_of_string id)))
+      | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
+
       | v = vernac_aux -> v ] 
     ]
   ;