From 1eb1083a4e135fba5a69c48af55333453a6a17df Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Feb 2015 19:04:37 +0100
Subject: STM: is Flags.async_proofs_full then always delegate

Probably a regression introduced in some code refactoring.
Affects only PIDE based code.
---
 stm/stm.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index 96a11d306d..693c673b40 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1554,6 +1554,7 @@ let async_policy () =
 let delegate name =
   let time = get_hint_bp_time name in
   time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
+              || !Flags.async_proofs_full
 
 let collect_proof keep cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
-- 
cgit v1.2.3