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 +++
 1 file changed, 3 insertions(+)

(limited to 'intf')

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].*)
-- 
cgit v1.2.3