[flags] Move global time flag into an attribute.

One less global flag.

19 files changed, 67 insertions, 70 deletions

diff --git a/API/API.mli b/API/API.mli
index 24a99d57f..892c05b64 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4294,7 +4294,7 @@ sig
 type vernac_control =
   | VernacExpr of vernac_expr
    (* Control *)
-  | VernacTime of vernac_control Loc.located
+  | VernacTime of bool * vernac_control Loc.located
   | VernacRedirect of string * vernac_control Loc.located
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index a90e5501a..5106e513b 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -479,8 +479,9 @@ and vernac_argument_status = {
 
 type vernac_control =
   | VernacExpr of vernac_expr
-   (* Control *)
-  | VernacTime of vernac_control located
+  (* boolean is true when the `-time` batch-mode command line flag was set.
+     the flag is used to print differently in `-time` vs `Time foo` *)
+  | VernacTime of bool * vernac_control located
   | VernacRedirect of string * vernac_control located
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control
diff --git a/lib/flags.ml b/lib/flags.ml
index 644f66d02..cd4a22d58 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -48,8 +48,6 @@ let profile = false
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
-let time = ref false
-
 let raw_print = ref false
 
 let univ_print = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 000862b2c..62328e3d3 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -35,9 +35,6 @@ val profile : bool
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
-(* -time option: every command will be wrapped with `Time` *)
-val time : bool ref
-
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 
diff --git a/lib/system.ml b/lib/system.ml
index 2c8dbac7c..e56736eb1 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -294,18 +294,18 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
   real (round (sstop -. sstart)) ++ str "s" ++
   str ")"
 
-let with_time time f x =
+let with_time ~batch f x =
   let tstart = get_time() in
-  let msg = if time then "" else "Finished transaction in " in
+  let msg = if batch then "" else "Finished transaction in " in
   try
     let y = f x in
     let tend = get_time() in
-    let msg2 = if time then "" else " (successful)" in
+    let msg2 = if batch then "" else " (successful)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
-    let msg = if time then "" else "Finished failing transaction in " in
-    let msg2 = if time then "" else " (failure)" in
+    let msg = if batch then "" else "Finished failing transaction in " in
+    let msg2 = if batch then "" else " (failure)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
diff --git a/lib/system.mli b/lib/system.mli
index c02bc9c8a..0c0cc9fae 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -104,4 +104,4 @@ val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.t
 
-val with_time : bool -> ('a -> 'b) -> 'a -> 'b
+val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c18c6810f..6ecc8355c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -67,7 +67,7 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
 GEXTEND Gram
   GLOBAL: vernac_control gallina_ext noedit_mode subprf;
   vernac_control: FIRST
-    [ [ IDENT "Time"; c = located_vernac -> VernacTime c
+    [ [ IDENT "Time"; c = located_vernac -> VernacTime (false,c)
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
       | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac_control -> VernacFail v
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 418d4a0b8..e88284fb1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1223,7 +1223,7 @@ open Decl_kinds
     let return = tag_vernac v in
     match v with
     | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v'
-    | VernacTime (_,v) ->
+    | VernacTime (_,(_,v)) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
     | VernacRedirect (s, (_,v)) ->
       return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
diff --git a/stm/stm.ml b/stm/stm.ml
index afb6fabcb..7045df0ed 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1935,15 +1935,16 @@ end = struct (* {{{ *)
   let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
     { indentation; verbose; loc; expr = e; strlen }
   =
-    let e, time, fail =
-      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
+    let e, time, batch, fail =
+      let rec find ~time ~batch ~fail = function
+        | VernacTime (batch,(_,e)) -> find ~time:true ~batch ~fail e
+        | VernacRedirect (_,(_,e)) -> find ~time ~batch ~fail e
+        | VernacFail e -> find ~time ~batch ~fail:true e
+        | e -> e, time, batch, fail in
+      find ~time:false ~batch:false ~fail:false e in
     let st = Vernacstate.freeze_interp_state `No in
     Vernacentries.with_fail st fail (fun () ->
-    (if time then System.with_time !Flags.time else (fun x -> x)) (fun () ->
+    (if time then System.with_time ~batch 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/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1291b7642..2fa47ba43 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -195,7 +195,7 @@ let classify_vernac e =
   let rec static_control_classifier ~poly = function
     | VernacExpr e -> static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
-    | VernacTime (_,e) | VernacRedirect (_, (_,e)) ->
+    | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
        static_control_classifier ~poly e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match static_control_classifier ~poly e with
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3a195c1df..176dfb3c9 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true
 let load_rc = ref true
 let no_load_rc () = load_rc := false
 
-let load_rcfile doc sid =
+let load_rcfile ~time doc sid =
   if !load_rc then
     try
       if !rcfile_specified then
         if CUnix.file_readable_p !rcfile then
-          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
+          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
@@ -43,7 +43,7 @@ let load_rcfile doc sid =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
+          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
 	with Not_found -> doc, sid
 	(*
 	Flags.if_verbose
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 60ed698b8..c3fd72754 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -13,7 +13,7 @@ val set_debug : unit -> unit
 val set_rcfile : string -> unit
 
 val no_load_rc : unit -> unit
-val load_rcfile : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val load_rcfile : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
 
 val push_include : string -> Names.DirPath.t -> bool -> unit
 (** [push_include phys_path log_path implicit] *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 910c81381..5c1b27c33 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -300,13 +300,13 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
     is caught and handled (i.e. not re-raised).
 *)
 
-let do_vernac doc sid =
+let do_vernac ~time doc sid =
   top_stderr (fnl());
   if !print_emacs then top_stderr (str (top_buffer.prompt doc));
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.process_expr doc sid (read_sentence ~doc sid (fst input))
+    Vernac.process_expr ~time doc sid (read_sentence ~doc sid (fst input))
   with
     | Stm.End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
@@ -337,13 +337,13 @@ let loop_flush_all () =
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
-let rec loop doc =
+let rec loop ~time doc =
   Sys.catch_break true;
   try
     reset_input_buffer doc stdin top_buffer;
     (* Be careful to keep this loop tail-recursive *)
     let rec vernac_loop doc sid =
-      let ndoc, nsid = do_vernac doc sid in
+      let ndoc, nsid = do_vernac ~time doc sid in
       loop_flush_all ();
       vernac_loop ndoc nsid
     (* We recover the current stateid, threading from the caller is
@@ -358,4 +358,4 @@ let rec loop doc =
                   fnl() ++
                   str"Please report" ++
                   strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
-      loop doc
+      loop ~time doc
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 46934f326..09240ec82 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,8 +32,8 @@ val coqloop_feed : Feedback.feedback -> unit
 
 (** Parse and execute one vernac command. *)
 
-val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
 
 (** Main entry point of Coq: read and execute vernac commands. *)
 
-val loop : Stm.doc -> Stm.doc
+val loop : time:bool -> Stm.doc -> Stm.doc
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 437b7b0ac..a3a4e20af 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -80,6 +80,7 @@ let toploop_init = ref begin fun x ->
    bogus. For now we just print to the console too *)
 let coqtop_init_feed = Coqloop.coqloop_feed
 let drop_last_doc = ref None
+let measure_time = ref false
 
 (* Default toplevel loop *)
 let console_toploop_run doc =
@@ -89,7 +90,7 @@ let console_toploop_run doc =
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
-  let doc = Coqloop.loop doc in
+  let doc = Coqloop.loop ~time:!measure_time doc in
   (* Initialise and launch the Ocaml toplevel *)
   drop_last_doc := Some doc;
   Coqinit.init_ocaml_path();
@@ -180,19 +181,19 @@ let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
   load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
 
-let load_vernacular doc sid =
+let load_vernacular ~time doc sid =
   List.fold_left
     (fun (doc,sid) (f_in, verbosely) ->
       let s = Loadpath.locate_file f_in in
       if !Flags.beautify then
-        Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
+        Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid) f_in
       else
-        Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
+        Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid s)
     (doc, sid) (List.rev !load_vernacular_list)
 
-let load_init_vernaculars doc sid =
-  let doc, sid = Coqinit.load_rcfile doc sid in
-  load_vernacular doc sid
+let load_init_vernaculars ~time doc sid =
+  let doc, sid = Coqinit.load_rcfile ~time doc sid in
+  load_vernacular ~time doc sid
 
 (******************************************************************************)
 (* Required Modules                                                           *)
@@ -291,7 +292,7 @@ let ensure_exists f =
     compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
-let compile ~verbosely ~f_in ~f_out =
+let compile ~time ~verbosely ~f_in ~f_out =
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
     if not (CList.is_empty pfs) then
@@ -316,7 +317,7 @@ let compile ~verbosely ~f_in ~f_out =
             require_libs = require_libs ()
           }) in
 
-      let doc, sid = load_init_vernaculars doc sid in
+      let doc, sid = load_init_vernaculars ~time doc sid in
       let ldir = Stm.get_ldir ~doc in
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_vo)
@@ -324,7 +325,7 @@ let compile ~verbosely ~f_in ~f_out =
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let doc, _ = Vernac.load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
       let _doc = Stm.join ~doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -351,10 +352,10 @@ let compile ~verbosely ~f_in ~f_out =
             require_libs = require_libs ()
           }) in
 
-      let doc, sid = load_init_vernaculars doc sid in
+      let doc, sid = load_init_vernaculars ~time doc sid in
 
       let ldir = Stm.get_ldir ~doc in
-      let doc, _ = Vernac.load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
       let doc = Stm.finish ~doc in
       check_pending_proofs ();
       let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
@@ -369,9 +370,9 @@ let compile ~verbosely ~f_in ~f_out =
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile ~verbosely ~f_in ~f_out =
+let compile ~time ~verbosely ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile ~verbosely ~f_in ~f_out;
+  compile ~time ~verbosely ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
 let compile_file (verbosely,f_in) =
@@ -381,9 +382,9 @@ let compile_file (verbosely,f_in) =
   else
     compile ~verbosely ~f_in ~f_out:None
 
-let compile_files doc =
+let compile_files ~time =
   if !compile_list == [] then ()
-  else List.iter compile_file (List.rev !compile_list)
+  else List.iter (compile_file ~time) (List.rev !compile_list)
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
@@ -736,7 +737,7 @@ let parse_args arglist =
     |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
     |"-quick" -> compilation_mode := BuildVio
     |"-list-tags" -> print_tags := true
-    |"-time" -> Flags.time := true
+    |"-time" -> measure_time := true
     |"-type-in-type" -> set_type_in_type ()
     |"-unicode" -> add_require ("Utf8_core", None, Some false)
     |"-v"|"--version" -> Usage.version (exitcode ())
@@ -812,12 +813,12 @@ let init_toplevel arglist =
                                 { doc_type = Interactive !toplevel_name;
                                   require_libs = require_libs ()
                                 }) in
-          Some (load_init_vernaculars doc sid)
+          Some (load_init_vernaculars ~time:!measure_time doc sid)
         with any -> flush_all(); fatal_error any
       (* Non interactive *)
       end else begin
         try
-          compile_files ();
+          compile_files ~time:!measure_time;
           schedule_vio_checking ();
           schedule_vio_compilation ();
           check_vio_tasks ();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 24d414c88..6b45a94bc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -110,16 +110,15 @@ let pr_open_cur_subgoals () =
 (*     Stm.End_of_input -> true *)
 (*   | _ -> false *)
 
-let rec interp_vernac ~check ~interactive doc sid (loc,com) =
+let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
   let interp v =
     match under_control v with
     | VernacLoad (verbosely, fname) ->
         let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-        load_vernac ~verbosely ~check ~interactive doc sid f
+        load_vernac ~time ~verbosely ~check ~interactive doc sid f
     | _ ->
-
       (* XXX: We need to run this before add as the classification is
          highly dynamic and depends on the structure of the
          document. Hopefully this is fixed when VtMeta can be removed
@@ -158,8 +157,8 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
     try
       (* The -time option is only supported from console-based
          clients due to the way it prints. *)
-      if !Flags.time then print_cmd_header ?loc com;
-      let com = if !Flags.time then VernacTime (loc,com) else com in
+      if time then print_cmd_header ?loc com;
+      let com = if time then VernacTime(time,(loc,com)) else com in
       interp com
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
@@ -173,7 +172,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
       end in iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac ~verbosely ~check ~interactive doc sid file =
+and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
   let ft_beautify, close_beautify =
     if !Flags.beautify_file then
       let chan_beautify = open_out (file^beautify_suffix) in
@@ -215,7 +214,7 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
-      let ndoc, nsid = Flags.silently (interp_vernac ~check ~interactive !rdoc !rsid) (loc, ast) in
+      let ndoc, nsid = Flags.silently (interp_vernac ~time ~check ~interactive !rdoc !rsid) (loc, ast) in
       rsid := nsid;
       rdoc := ndoc
     done;
@@ -242,6 +241,6 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let process_expr doc sid loc_ast =
+let process_expr ~time doc sid loc_ast =
   checknav_deep loc_ast;
-  interp_vernac ~interactive:true ~check:true doc sid loc_ast
+  interp_vernac ~time ~interactive:true ~check:true doc sid loc_ast
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 8a798a98e..b77b024fa 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,9 +12,9 @@
     expected to handle and print errors in form of exceptions, however
     care is taken so the state machine is left in a consistent
     state. *)
-val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
+val process_expr : time:bool -> Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle
     and print errors in form of exceptions. *)
-val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
+val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index aa6121c39..7aa27dcdf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2213,8 +2213,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
       control v
   | VernacRedirect (s, (_,v)) ->
        Topfmt.with_output_to_file s control v
-  | VernacTime (_,v) ->
-      System.with_time !Flags.time control v;
+  | VernacTime (batch, (_loc,v)) ->
+      System.with_time ~batch control v;
 
   and aux ?polymorphism ~atts isprogcmd = function
 
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 4a01ef2ef..bd2d0261a 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -14,14 +14,14 @@ open Vernacexpr
 let rec under_control = function
   | VernacExpr c -> c
   | VernacRedirect (_,(_,c))
-  | VernacTime (_,c)
+  | VernacTime (_,(_,c))
   | VernacFail c
   | VernacTimeout (_,c) -> under_control c
 
 let rec has_Fail = function
   | VernacExpr c -> false
   | VernacRedirect (_,(_,c))
-  | VernacTime (_,c)
+  | VernacTime (_,(_,c))
   | VernacTimeout (_,c) -> has_Fail c
   | VernacFail _ -> true
 
@@ -38,7 +38,7 @@ let is_navigation_vernac c =
   is_navigation_vernac_expr (under_control c)
 
 let rec is_deep_navigation_vernac = function
-  | VernacTime (_,c) -> is_deep_navigation_vernac c
+  | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c
   | VernacRedirect (_, (_,c))
   | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
   | VernacExpr _ -> false