diff options
| -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,_) -> |