diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-23 11:12:28 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:48:44 -0400 |
| commit | f6cea698f19766087fa56b16ed8dc8cedf079643 (patch) | |
| tree | 1880e497e1f4228cabf4e712c80fd9ff5b2ad3d0 /stm/vernac_classifier.ml | |
| parent | 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 (diff) | |
STM: proof block detection for bullets and { block }
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 13 |
1 files changed, 10 insertions, 3 deletions
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 |