diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 71ec8acc68..822229f47e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1746,12 +1746,13 @@ end = struct (* {{{ *) { indentation; verbose; loc; expr = e; strlen } = let e, time, fail = - let rec find time fail = function - | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e - | VernacFail e -> find time true e - | _ -> e, time, fail in find false false e in + let rec find ~time ~fail = function + | VernacTime (_,e) -> find ~time:true ~fail e + | VernacRedirect (_,(_,e)) -> find ~time ~fail e + | VernacFail e -> find ~time ~fail:true e + | e -> e, time, fail in find ~time:false ~fail:false e in Hooks.call Hooks.with_fail fail (fun () -> - (if time then System.with_time false else (fun x -> x)) (fun () -> + (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let goals, _, _, _, _ = Proof.proof p in @@ -2140,10 +2141,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; |