diff options
| author | Enrico Tassi | 2016-06-07 09:57:09 -0400 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-07 09:57:09 -0400 |
| commit | 4dcd50dd2767c60f8f773fb4ca1c3d4bc68819c8 (patch) | |
| tree | 424b1f5391e453d5e7964071fac9ec6aa99e9be9 /stm | |
| parent | 7a9462ce9a3d70ca43c363da3a0782f59c16a120 (diff) | |
Documentation
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 5 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
3 files changed, 6 insertions, 3 deletions
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"]) |