From 3abbc93733b7f820a436beedcd0b9292378e1840 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 30 Jun 2014 23:25:19 +0200
Subject: option to always delegate futures to workers

---
 stm/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index f62bae4b12..2007dba811 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1151,9 +1151,11 @@ let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 let delegate_policy_check time =
   if interactive () = `Yes then
     (!Flags.async_proofs_mode = Flags.APonParallel 0 ||
-    !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0
+    !Flags.async_proofs_mode = Flags.APonLazy) &&
+    (time >= 1.0 || !Flags.async_proofs_always_delegate)
   else if !Flags.compilation_mode = Flags.BuildVi then true
-  else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0
+  else !Flags.async_proofs_mode <> Flags.APoff &&
+       (time >= 1.0 || !Flags.async_proofs_always_delegate)
 
 let collect_proof cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
-- 
cgit v1.2.3