diff options
| author | Enrico Tassi | 2014-01-14 13:35:42 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-14 13:36:37 +0100 |
| commit | 9d4830afabb63f701532b588da31fb0d6ccce62c (patch) | |
| tree | 81d3c21e54f785c480efda5a7620f2f9faef87be | |
| parent | b8d31eb7f359dd842c1b53b1b74725158fc01c1e (diff) | |
STM: fix -async-proofs lazy
| -rw-r--r-- | toplevel/stm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |