diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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); |