From 1d4c34c79624fb81e64dfed8874b2fc9fa66c070 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Jan 2017 13:51:37 +0100
Subject: Process Next Obligation proofs in parallel (fix #5314)

---
 intf/vernacexpr.mli    | 3 +++
 ltac/g_obligations.ml4 | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 92e4dd618e..c9fb1b5986 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -524,6 +524,9 @@ and vernac_control =
   | VtObserve of Stateid.t
   | VtBack of Stateid.t
   | VtPG
+(* Qed typically generates an opaque proof term.  Still, by declaring
+ * a proof terminator one can use such opaque term to generate transparent
+ * ones.  In this corner case the STM needs to know... *)
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index 987b9d5387..2ae183e6e9 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -66,7 +66,7 @@ GEXTEND Gram
 
 open Obligations
 
-let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater)
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
 | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
-- 
cgit v1.2.3