diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b592aab0da..b0ad3f8790 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2232,10 +2232,13 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - resilient_command reach view.next; - stm_vernac_interp id x; - if eff then update_global_env () - ), (if eff then `Yes else cache), true + (match !Flags.async_proofs_mode with + | Flags.APon | Flags.APonLazy -> + resilient_command reach view.next + | Flags.APoff -> reach view.next); + stm_vernac_interp id x; + if eff then update_global_env () + ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; stm_vernac_interp id x; |