From f6cea698f19766087fa56b16ed8dc8cedf079643 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 23 May 2016 11:12:28 +0200
Subject: STM: proof block detection for bullets and { block }

---
 stm/vernac_classifier.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'stm/vernac_classifier.ml')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index aa9907045..11e973bf5 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -108,12 +108,19 @@ let rec classify_vernac e =
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
     | VernacProof _ 
-    | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
-    | VernacSubproof _ | VernacEndSubproof
+    | VernacSubproof _
     | VernacCheckGuard
     | VernacUnfocused
-    | VernacSolveExistential _ -> VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+    | VernacSolveExistential _ ->
+        VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+    | VernacBullet _ ->
+        VtProofStep { parallel = false; proof_block_detection = Some "bullet" },
+        VtLater
+    | VernacEndSubproof -> 
+        VtProofStep { parallel = false;
+                      proof_block_detection = Some "proof-block" },
+        VtLater
     (* Options changing parser *)
     | VernacUnsetOption (["Default";"Proof";"Using"])
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
-- 
cgit v1.2.3