12 files changed, 23 insertions, 88 deletions
diff --git a/lib/profile.ml b/lib/cProfile.ml
index 0bc226a45..0bc226a45 100644
--- a/lib/profile.ml
+++ b/lib/cProfile.ml
diff --git a/lib/profile.mli b/lib/cProfile.mli
index cae4397a1..cae4397a1 100644
--- a/lib/profile.mli
+++ b/lib/cProfile.mli
diff --git a/lib/control.ml b/lib/control.ml
index d936d7557..c6489938e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -12,15 +12,12 @@ let interrupt = ref false
 
 let steps = ref 0
 
-let are_we_threading = lazy (
-  match !Flags.async_proofs_mode with
-  | Flags.APon -> true
-  | _ -> false)
+let enable_thread_delay = ref false
 
 let check_for_interrupt () =
   if !interrupt then begin interrupt := false; raise Sys.Break end;
   incr steps;
-  if !steps = 1000 && Lazy.force are_we_threading then begin
+  if !enable_thread_delay && !steps = 1000 then begin
     Thread.delay 0.001;
     steps := 0;
   end
diff --git a/lib/control.mli b/lib/control.mli
index f6c63ffb3..261b07693 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -8,6 +8,9 @@
 
 (** Global control of Coq. *)
 
+(** Will periodically call [Thread.delay] if set to true *)
+val enable_thread_delay : bool ref
+
 val interrupt : bool ref
 (** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 83e673d2c..64535d35f 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -55,6 +55,8 @@ sig
   include PreS
 
   module Easy : sig
+
+    val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
     val make_dyn : string -> ('a -> t) * (t -> 'a)
     val inj : 'a -> 'a tag -> t
     val prj : t -> 'a tag -> 'a option
@@ -129,8 +131,9 @@ end
 include Self
 
 module Easy = struct
+
 (* now tags are opaque, we can do the trick *)
-let make_dyn (s : string) =
+let make_dyn_tag (s : string) =
  (fun (type a) (tag : a tag) ->
   let infun : (a -> t) = fun x -> Dyn (tag, x) in
   let outfun : (t -> a) = fun (Dyn (t, x)) ->
@@ -138,9 +141,12 @@ let make_dyn (s : string) =
     | None -> assert false
     | Some CSig.Refl -> x
   in
-  (infun, outfun))
+  infun, outfun, tag)
  (create s)
 
+let make_dyn (s : string) =
+  let inf, outf, _ = make_dyn_tag s in inf, outf
+
 let inj x tag = Dyn(tag,x)
 let prj : type a. t -> a tag -> a option =
     fun (Dyn(tag',x)) tag ->
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e0e1a9d14..2206394e2 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -53,6 +53,7 @@ val dump : unit -> (int * string) list
 module Easy : sig
 
   (* To create a dynamic type on the fly *)
+  val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
   val make_dyn : string -> ('a -> t) * (t -> 'a)
 
   (* For types declared with the [create] function above *)
diff --git a/lib/envars.ml b/lib/envars.ml
index 206d75033..8ebf84057 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -153,19 +153,17 @@ let coqpath =
 
 let exe s = s ^ Coq_config.exec_extension
 
-let ocamlfind () =
-  if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind
+let ocamlfind () = Coq_config.ocamlfind
 
 (** {2 Camlp4 paths} *)
 
 let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4)
 
 let camlp4bin () =
-  if !Flags.camlp4bin_spec then !Flags.camlp4bin else
-    if !Flags.boot then Coq_config.camlp4bin else
-      try guess_camlp4bin ()
-      with Not_found ->
-        Coq_config.camlp4bin
+  if !Flags.boot then Coq_config.camlp4bin else
+    try guess_camlp4bin ()
+    with Not_found ->
+      Coq_config.camlp4bin
 
 let camlp4 () = camlp4bin () / exe Coq_config.camlp4
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 5079b4b01..fb6e48ae2 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -35,36 +35,10 @@ let record_aux_file = ref false
 
 let test_mode = ref false
 
-type async_proofs = APoff | APonLazy | APon
-let async_proofs_mode = ref APoff
-type cache = Force
-let async_proofs_cache = ref None
-let async_proofs_n_workers = ref 1
-let async_proofs_n_tacworkers = ref 2
-let async_proofs_private_flags = ref None
-let async_proofs_full = ref false
-let async_proofs_never_reopen_branch = ref false
-let async_proofs_flags_for_workers = ref []
 let async_proofs_worker_id = ref "master"
-type priority = Low | High
-let async_proofs_worker_priority = ref Low
-let string_of_priority = function Low -> "low" | High -> "high"
-let priority_of_string = function
-  | "low" -> Low
-  | "high" -> High
-  | _ -> raise (Invalid_argument "priority_of_string")
-type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "curly" ])
-let async_proofs_cmd_error_resilience = ref true
-
-let async_proofs_is_worker () =
-  !async_proofs_worker_id <> "master"
-let async_proofs_is_master () =
-  !async_proofs_mode = APon && !async_proofs_worker_id = "master"
-let async_proofs_delegation_threshold = ref 0.03
+let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
 let debug = ref false
-let stm_debug = ref false
 
 let in_debugger = ref false
 let in_toplevel = ref false
@@ -179,14 +153,6 @@ let is_standard_doc_url url =
 let coqlib_spec = ref false
 let coqlib = ref "(not initialized yet)"
 
-(* Options for changing ocamlfind (used by coqmktop) *)
-let ocamlfind_spec = ref false
-let ocamlfind = ref Coq_config.camlbin
-
-(* Options for changing camlp4bin (used by coqmktop) *)
-let camlp4bin_spec = ref false
-let camlp4bin = ref Coq_config.camlp4bin
-
 (* Level of inlining during a functor application *)
 
 let default_inline_level = 100
diff --git a/lib/flags.mli b/lib/flags.mli
index 8825390e6..58415d6f5 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,35 +21,14 @@ val record_aux_file : bool ref
 val test_mode : bool ref
 
 (** Async-related flags *)
-type async_proofs = APoff | APonLazy | APon
-val async_proofs_mode : async_proofs ref
-type cache = Force
-val async_proofs_cache : cache option ref
-val async_proofs_n_workers : int ref
-val async_proofs_n_tacworkers : int ref
-val async_proofs_private_flags : string option ref
-val async_proofs_is_worker : unit -> bool
-val async_proofs_is_master : unit -> bool
-val async_proofs_full : bool ref
-val async_proofs_never_reopen_branch : bool ref
-val async_proofs_flags_for_workers : string list ref
 val async_proofs_worker_id : string ref
-type priority = Low | High
-val async_proofs_worker_priority : priority ref
-val string_of_priority : priority -> string
-val priority_of_string : string -> priority
-type tac_error_filter = [ `None | `Only of string list | `All ]
-val async_proofs_tac_error_resilience : tac_error_filter ref
-val async_proofs_cmd_error_resilience : bool ref
-val async_proofs_delegation_threshold : float ref
+val async_proofs_is_worker : unit -> bool
 
+(** Debug flags *)
 val debug : bool ref
 val in_debugger : bool ref
 val in_toplevel : bool ref
 
-(** Enable STM debugging *)
-val stm_debug : bool ref
-
 val profile : bool
 
 (* -ide_slave: printing will be more verbose, will affect stm caching *)
@@ -143,12 +122,6 @@ val is_standard_doc_url : string -> bool
 val coqlib_spec : bool ref
 val coqlib : string ref
 
-(** Options for specifying where OCaml binaries reside *)
-val ocamlfind_spec : bool ref
-val ocamlfind : string ref
-val camlp4bin_spec : bool ref
-val camlp4bin : string ref
-
 (** Level of inlining during a functor application *)
 val set_inline_level : int -> unit
 val get_inline_level : unit -> int
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 8791f0741..66f939a91 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -9,7 +9,7 @@ System
 CThread
 Spawn
 Trie
-Profile
+CProfile
 Explore
 Predicate
 Rtree
diff --git a/lib/system.ml b/lib/system.ml
index 4b5066ef4..2c8dbac7c 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -309,9 +309,3 @@ let with_time time f x =
     let msg2 = if time then "" else " (failure)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
-
-let process_id () =
-  Printf.sprintf "%d:%s:%d" (Unix.getpid ())
-    (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
-     else "master")
-    (Thread.id (Thread.self ()))
diff --git a/lib/system.mli b/lib/system.mli
index aa964abeb..c02bc9c8a 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -105,6 +105,3 @@ val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.t
 
 val with_time : bool -> ('a -> 'b) -> 'a -> 'b
-
-(** {6 Name of current process.} *)
-val process_id : unit -> string