aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml11
1 files changed, 7 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index f577994ffa..56243b76f9 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2136,10 +2136,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;
- 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);
+ 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;
vernac_interp id x;