6 files changed, 9 insertions, 31 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 34f9aed37b..1e52af0be7 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -11,7 +11,6 @@ type project = {
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
-  bypass_API : bool;
 
   v_files : string list;
   mli_files : string list;
@@ -43,12 +42,11 @@ and install =
   | UserInstall
 
 (* TODO generate with PPX *)
-let mk_project project_file makefile install_kind use_ocamlopt bypass_API = {
+let mk_project project_file makefile install_kind use_ocamlopt = {
   project_file;
   makefile;
   install_kind;
   use_ocamlopt;
-  bypass_API;
 
   v_files = [];
   mli_files = [];
@@ -181,8 +179,6 @@ let process_cmd_line orig_dir proj args =
     aux { proj with defs = proj.defs @ [v,def] } r
   | "-arg" :: a :: r ->
     aux { proj with extra_args = proj.extra_args @ [a] } r
-  | "-bypass-API" :: r ->
-    aux { proj with bypass_API = true } r
   | f :: r ->
       let f = CUnix.correct_path f orig_dir in
       let proj =
@@ -202,11 +198,11 @@ let process_cmd_line orig_dir proj args =
  (******************************* API ************************************)
 
 let cmdline_args_to_project ~curdir args =
-  process_cmd_line curdir (mk_project None None None true false) args
+  process_cmd_line curdir (mk_project None None None true) args
 
 let read_project_file f =
   process_cmd_line (Filename.dirname f)
-    (mk_project (Some f) None (Some NoInstall) true false) (parse f)
+    (mk_project (Some f) None (Some NoInstall) true) (parse f)
 
 let rec find_project_file ~from ~projfile_name =
   let fname = Filename.concat from projfile_name in
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 23a27a54ab..810189450f 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -13,7 +13,6 @@ type project = {
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
-  bypass_API : bool;
 
   v_files : string list;
   mli_files : string list;
diff --git a/lib/flags.ml b/lib/flags.ml
index 644f66d02b..ee4c0734af 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 000862b2c6..33d281798f 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 2c8dbac7c0..e56736eb15 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 c02bc9c8ac..0c0cc9fae5 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