Fix a few programming pearls related to Time, Fail and Redirect.

This fixes a few clear bugs, but the STM code handling Time, Fail and
Redirect before par: still needs to be rewritten. It does not implement
the same semantics as the vernac interpreter for Fail Fail [c] and
ignores Redirect.

This commit was already reviewed with Enrico and tested on Travis.

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;