diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index b1df3c9ca..aa9907045 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -21,8 +21,9 @@ let string_of_vernac_type = function | VtQed VtKeep -> "Qed(keep)" | VtQed VtKeepAsAxiom -> "Qed(admitted)" | VtQed VtDrop -> "Qed(drop)" - | VtProofStep false -> "ProofStep" - | VtProofStep true -> "ProofStep (parallel)" + | VtProofStep { parallel; proof_block_detection } -> + "ProofStep " ^ if parallel then "par " else "" ^ + Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ @@ -93,7 +94,9 @@ let rec classify_vernac e = (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ | VtStm _ | VtProofMode _ ), _ as x -> x - | VtQed _, _ -> VtProofStep false, VtNow + | VtQed _, _ -> + VtProofStep { parallel = false; proof_block_detection = None }, + VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater @@ -110,7 +113,7 @@ let rec classify_vernac e = | VernacSubproof _ | VernacEndSubproof | VernacCheckGuard | VernacUnfocused - | VernacSolveExistential _ -> VtProofStep false, VtLater + | VernacSolveExistential _ -> VtProofStep { parallel = false; proof_block_detection = None }, VtLater (* Options changing parser *) | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow @@ -219,4 +222,4 @@ let rec classify_vernac e = let classify_as_query = VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater let classify_as_sideeff = VtSideff [], VtLater -let classify_as_proofstep = VtProofStep false, VtLater +let classify_as_proofstep = VtProofStep { parallel = false; proof_block_detection = None}, VtLater |