Merge branch 'v8.6' into trunk

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;