From 6ff62ec78d5517ec5905041fa2e4926e15ff89f0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 21 Jan 2017 07:51:15 +0100
Subject: Revert "Process Next Obligation proofs in parallel (fix #5314)"

This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070.

It seems the proof terminator of obligation.ml, in the case in which
Set Shrink Obligation is set, accesses the opaque proof.
---
 intf/vernacexpr.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index c9fb1b5986..92e4dd618e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -524,9 +524,6 @@ 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