From 4dcd50dd2767c60f8f773fb4ca1c3d4bc68819c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 7 Jun 2016 09:57:09 -0400
Subject: Documentation

---
 stm/proofBlockDelimiter.ml | 2 +-
 stm/stm.ml                 | 5 ++++-
 stm/vernac_classifier.ml   | 2 +-
 3 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index ed8553d4b9..ce12185cba 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -127,7 +127,7 @@ let dynamic_curly_brace { dynamic_switch = id } =
   | `Not -> `Leaks
 
 let () = register_proof_block_delimiter
-  "proof-block" static_curly_brace dynamic_curly_brace
+  "curly" static_curly_brace dynamic_curly_brace
 
 (* ***************** par: ************************************************* *)
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 3ac1f98925..75d2e070ae 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -238,7 +238,10 @@ let default_info () =
 module DynBlockData : Dyn.S = Dyn.Make(struct end)
 
 (* Clusters of nodes implemented as Dag properties.  While Dag and Vcs impose
- * no constraint on properties, here we impose boxes to be non overlapping. *)
+ * no constraint on properties, here we impose boxes to be non overlapping.
+ * Such invariant makes sense for the current kinds of boxes (proof blocks and
+ * entire proofs) but may make no sense and dropped/refined in the future.
+ * Such invariant is useful to detect broken proof block detection code *)
 type box =
   | ProofTask of pt
   | ProofBlock of static_block_declaration * proof_block_name
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 11e973bf56..a602d6b8a8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -119,7 +119,7 @@ let rec classify_vernac e =
         VtLater
     | VernacEndSubproof -> 
         VtProofStep { parallel = false;
-                      proof_block_detection = Some "proof-block" },
+                      proof_block_detection = Some "curly" },
         VtLater
     (* Options changing parser *)
     | VernacUnsetOption (["Default";"Proof";"Using"])
-- 
cgit v1.2.3