diff options
| -rw-r--r-- | toplevel/vernac_classifier.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 4ef157a64a..37ab694b6d 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -73,7 +73,7 @@ let rec classify_vernac e = | VernacTime e -> classify_vernac e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with - | ( VtQuery _ | VtProofStep _ | VtSideff _ + | ( VtQuery _ | VtProofStep | VtSideff _ | VtStm _ | VtProofMode _ ), _ as x -> x | VtQed _, _ -> VtProofStep, VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) @@ -86,11 +86,11 @@ let rec classify_vernac e = (* ProofStep *) | VernacProof _ | VernacBullet _ - | VernacFocus _ | VernacUnfocus _ - | VernacSubproof _ | VernacEndSubproof _ + | VernacFocus _ | VernacUnfocus + | VernacSubproof _ | VernacEndSubproof | VernacSolve _ | VernacError _ - | VernacCheckGuard _ - | VernacUnfocused _ + | VernacCheckGuard + | VernacUnfocused | VernacSolveExistential _ -> VtProofStep, VtLater (* StartProof *) | VernacDefinition (_,(_,i),ProveBody _) -> @@ -169,7 +169,7 @@ let rec classify_vernac e = (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ - | VernacResetName _ | VernacResetInitial _ + | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e (* What are these? *) | VernacNop |