diff options
| -rw-r--r-- | stm/stm.ml | 11 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
2 files changed, 7 insertions, 6 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 56243b76f9..3efad70fb2 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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6736d83293..3df6d7a580 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2218,7 +2218,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v | VernacRedirect (s, (_,v)) -> - Feedback.with_output_to_file s (aux false) v + Feedback.with_output_to_file s (aux ?locality ?polymorphism isprogcmd) v | VernacTime (_,v) -> System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v; |