From ddb0fc8abb8b6cb06e238bc63be0a21d4cea3cbc Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 Aug 2014 20:22:30 +0200
Subject: STM: Classify Let as non asynchronous (Closes: #3486)

---
 stm/vernac_classifier.ml | 3 +++
 1 file changed, 3 insertions(+)

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,_) ->
-- 
cgit v1.2.3