From 9d4830afabb63f701532b588da31fb0d6ccce62c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 14 Jan 2014 13:35:42 +0100
Subject: STM: fix -async-proofs lazy

---
 toplevel/stm.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 521af61e3a..fc888eea78 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1115,7 +1115,9 @@ end = struct (* {{{ *)
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
 let delegate_policy_check () =
-  if interactive () = `Yes then !Flags.async_proofs_mode = Flags.APonParallel 0
+  if interactive () = `Yes then
+    !Flags.async_proofs_mode = Flags.APonParallel 0 ||
+    !Flags.async_proofs_mode = Flags.APonLazy
   else if !Flags.compilation_mode = Flags.BuildVi then true
   else !Flags.async_proofs_mode <> Flags.APoff
 
-- 
cgit v1.2.3