diff options
| author | Enrico Tassi | 2013-12-26 17:07:53 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-05 16:55:58 +0100 |
| commit | 738440cdf663f5d2cb4d8e4f186b1accb9dac81d (patch) | |
| tree | 43cf72992df2d3072a8e7f033e3184083d519df8 | |
| parent | 85e5450775fd8cfaefa8962c9907941aa8154274 (diff) | |
Fix some warnings with ocamlc 4.01
| -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 |