4 files changed, 6 insertions, 23 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 644f66d02..ee4c0734a 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
@@ -110,14 +108,6 @@ let universe_polymorphism = ref false
 let make_universe_polymorphism b = universe_polymorphism := b
 let is_universe_polymorphism () = !universe_polymorphism
 
-let local_polymorphic_flag = ref None
-let use_polymorphic_flag () = 
-  match !local_polymorphic_flag with 
-  | Some p -> local_polymorphic_flag := None; p
-  | None -> is_universe_polymorphism ()
-let make_polymorphic_flag b =
-  local_polymorphic_flag := Some b
-
 let polymorphic_inductive_cumulativity = ref false
 let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
 let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
diff --git a/lib/flags.mli b/lib/flags.mli
index 000862b2c..33d281798 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
 
@@ -77,10 +74,6 @@ val is_program_mode : unit -> bool
 val make_universe_polymorphism : bool -> unit
 val is_universe_polymorphism : unit -> bool
 
-(** Local universe polymorphism flag. *)
-val make_polymorphic_flag : bool -> unit
-val use_polymorphic_flag : unit -> bool
-
 (** Global polymorphic inductive cumulativity flag. *)
 val make_polymorphic_inductive_cumulativity : bool -> unit
 val is_polymorphic_inductive_cumulativity : unit -> bool
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