diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-08 13:17:06 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-09 13:11:38 +0200 |
| commit | 9d443eb0ff815a804f771335f0ac38a94d2851f2 (patch) | |
| tree | 3e98143409529e20f61169ea7dc1039376139a8b /stm/vernac_classifier.ml | |
| parent | de5ed8e17df8433d4f0ffe6a6440505b5a530638 (diff) | |
Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index ce9c2b3ff..6ad1294fc 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -17,6 +17,7 @@ let string_of_vernac_type = function | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" | VtQed VtKeep -> "Qed(keep)" + | VtQed VtKeepAsAxiom -> "Qed(admitted)" | VtQed VtDrop -> "Qed(drop)" | VtProofStep false -> "ProofStep" | VtProofStep true -> "ProofStep (parallel)" @@ -86,7 +87,8 @@ let rec classify_vernac e = | VtQed _, _ -> VtProofStep false, VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) (* Qed *) - | VernacEndProof Admitted | VernacAbort _ -> VtQed VtDrop, VtLater + | VernacAbort _ -> VtQed VtDrop, VtLater + | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ |