From 84accdaea3ce094cc5d0232107d3e2ea654a76c2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 18 Sep 2017 13:27:20 +0200
Subject: Remove STM vernaculars.

---
 parsing/g_vernac.ml4 | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index de98415cd6..0da22fd71c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -75,10 +75,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 "Wait"; "." -> VernacStm Wait
-
       | v = vernac_poly -> v ]
     ]
   ;
-- 
cgit v1.2.3