From 4703e70b4086bcc14fdd06b3afd98cad0b45157f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 15 Oct 2014 08:40:13 +0200
Subject: Fix -async-proofs-always-delegate (close 3740)

---
 stm/stm.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'stm/stm.ml')

diff --git a/stm/stm.ml b/stm/stm.ml
index 450259eec..705d427f4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1228,8 +1228,7 @@ let collect_proof keep cur hd brkind id =
         else `Sync (name,proof_using_ast last,`Policy)
     | `Fork((_, hd', GuaranteesOpacity, ids), _) when
        has_proof_no_using last && not (State.is_cached (parent last)) &&
-       (!Flags.compilation_mode = Flags.BuildVi ||
-        !Flags.async_proofs_always_delegate) ->
+       !Flags.compilation_mode = Flags.BuildVi ->
         (try
           let name = name ids in
           let hint, time = get_hint_ctx loc, get_hint_bp_time name in
-- 
cgit v1.2.3