Merge PR #6433: [flags] Move global time flag into an attribute.

2 files changed, 5 insertions, 5 deletions

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