diff options
| author | Enrico Tassi | 2014-08-04 20:22:30 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-08-05 18:24:50 +0200 |
| commit | ddb0fc8abb8b6cb06e238bc63be0a21d4cea3cbc (patch) | |
| tree | c442e671eae21b99dcbf59f4795a45dc71151ce5 | |
| parent | 35ff66308bee60f5c0e0e917a8ad4b817bc36851 (diff) | |
STM: Classify Let as non asynchronous (Closes: #3486)
| -rw-r--r-- | stm/vernac_classifier.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dac5e5ae88..2b8c36ca96 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -103,6 +103,9 @@ let rec classify_vernac e = | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) + | VernacDefinition ( + (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) -> + VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,(_,i),ProveBody _) -> VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater | VernacStartTheoremProof (_,l,_) -> |