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 ---
 ltac/g_obligations.ml4 | 2 +-
 2 files changed, 1 insertion(+), 4 deletions(-)

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].*)
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index 2ae183e6e9..987b9d5387 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",GuaranteesOpacity,[]), VtLater)
+let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
 | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
-- 
cgit v1.2.3