Imported Upstream version 8.9.0upstream/8.9.0upstream

22 files changed, 690 insertions, 143 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 97502211..811fcf40 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -47,8 +47,6 @@ exception AlreadyDeclared of Pp.t (* for already declared Schemes *)
 let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
 exception Timeout
-exception Drop
-exception Quit
 
 let handle_stack = ref []
 
@@ -126,7 +124,7 @@ end
 let noncritical = function
   | Sys.Break | Out_of_memory | Stack_overflow
   | Assert_failure _ | Match_failure _ | Anomaly _
-  | Timeout | Drop | Quit -> false
+  | Timeout -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
 [@@@ocaml.warning "+52"]
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index ec34dd62..4e2fe762 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -53,8 +53,6 @@ val invalid_arg : ?loc:Loc.t -> string -> 'a
 val todo : string -> unit
 
 exception Timeout
-exception Drop
-exception Quit
 
 (** [register_handler h] registers [h] as a handler.
     When an expression is printed with [print e], it
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index fda25a0a..0cf989e4 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -120,7 +120,7 @@ let uniquize_flags_rev flags =
 
 (** [normalize_flags] removes redundant warnings. Unknown warnings are kept
     because they may be declared in a plugin that will be linked later. *)
-let normalize_flags ~silent warnings =
+let normalize_flags warnings =
   let warnings = cut_before_all_rev warnings in
   uniquize_flags_rev warnings
 
@@ -130,7 +130,7 @@ let normalize_flags_string s =
   if is_none_keyword s then s
   else
     let flags = flags_of_string s in
-    let flags = normalize_flags ~silent:false flags in
+    let flags = normalize_flags flags in
     string_of_flags flags
 
 let parse_warnings items =
@@ -146,7 +146,7 @@ let parse_flags s =
   else begin
       Flags.make_warn true;
       let flags = flags_of_string s in
-      let flags = normalize_flags ~silent:true flags in
+      let flags = normalize_flags flags in
       parse_warnings flags;
       string_of_flags flags
     end
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml
index d6c340f6..c2bcd73f 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml
@@ -8,6 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* This needs to go trou feedback as it is invoked from IDEs, but
+   ideally we would like to make this independent so it can be
+   bootstrapped. *)
+
+(* Note the problem with the error invokation below calling exit... *)
+(* let error msg = Feedback.msg_error msg *)
+let warning msg = Feedback.msg_warning Pp.(str msg)
+
 type arg_source = CmdLine | ProjectFile
 
 type 'a sourced = { thing : 'a; source : arg_source }
@@ -82,30 +90,50 @@ let rec post_canonize f =
 
 exception Parsing_error of string
 
-let rec parse_string = parser
-  | [< '' ' | '\n' | '\t' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
-  | [< >] -> ""
-and parse_string2 = parser
-  | [< ''"' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
-  | [< >] -> raise (Parsing_error "unterminated string")
-and parse_skip_comment = parser
-  | [< ''\n'; s >] -> s
-  | [< 'c; s >] -> parse_skip_comment s
-  | [< >] -> [< >]
-and parse_args = parser
-  | [< '' ' | '\n' | '\t'; s >] -> parse_args s
-  | [< ''#'; s >] -> parse_args (parse_skip_comment s)
-  | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
-  | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
-  | [< >] -> []
+let buffer buf =
+  let ans = Buffer.contents buf in
+  let () = Buffer.clear buf in
+  ans
+
+let rec parse_string buf s = match Stream.next s with
+| ' ' | '\n' | '\t' -> buffer buf
+| c ->
+  let () = Buffer.add_char buf c in
+  parse_string buf s
+| exception Stream.Failure -> buffer buf
+
+and parse_string2 buf s = match Stream.next s with
+| '"' -> buffer buf
+| c ->
+  let () = Buffer.add_char buf c in
+  parse_string2 buf s
+| exception Stream.Failure -> raise (Parsing_error "unterminated string")
+
+and parse_skip_comment s = match Stream.next s with
+| '\n' -> ()
+| _ -> parse_skip_comment s
+| exception Stream.Failure -> ()
+
+and parse_args buf accu s = match Stream.next s with
+| ' ' | '\n' | '\t' -> parse_args buf accu s
+| '#' ->
+  let () = parse_skip_comment s in
+  parse_args buf accu s
+| '"' ->
+  let str = parse_string2 buf s in
+  parse_args buf (str :: accu) s
+| c ->
+  let () = Buffer.add_char buf c in
+  let str = parse_string buf s in
+  parse_args buf (str :: accu) s
+| exception Stream.Failure -> accu
 
 let parse f =
   let c = open_in f in
-  let res = parse_args (Stream.of_channel c) in
+  let buf = Buffer.create 64 in
+  let res = parse_args buf [] (Stream.of_channel c) in
   close_in c;
-  res
+  List.rev res
 ;;
 
 (* Copy from minisys.ml, since we don't see that file here *)
@@ -122,7 +150,7 @@ let process_cmd_line orig_dir proj args =
   let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
   let orig_dir = (* avoids turning foo.v in ./foo.v *)
     if orig_dir = "." then "" else orig_dir in
-  let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
+  let error s = (Format.eprintf "Error: @[%s@].@\n%!" s; exit 1) in
   let mk_path d =
     let p = CUnix.correct_path d orig_dir in
     { path = CUnix.remove_path_dot (post_canonize p);
@@ -135,12 +163,12 @@ let process_cmd_line orig_dir proj args =
     error "Use \"-install none\" instead of \"-no-install\""
   | "-custom" :: _ ->
     error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\""
-  
+
   | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt =  false } r
   | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt =  true } r
   | "-install" :: d :: r ->
     if proj.install_kind <> None then
-      Feedback.msg_warning (Pp.str "-install set more than once.");
+      (warning "-install set more than once.@\n%!");
     let install = match d with
       | "user" -> UserInstall
       | "none" -> NoInstall
@@ -167,8 +195,7 @@ let process_cmd_line orig_dir proj args =
     let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
     let () = match proj.project_file with
       | None -> ()
-      | Some _ -> Feedback.msg_warning (Pp.str
-	"Multiple project files are deprecated.")
+      | Some _ -> warning "Multiple project files are deprecated.@\n%!"
     in
     parsing_project_file := true;
     let proj = aux { proj with project_file = Some file } (parse file) in
@@ -182,7 +209,7 @@ let process_cmd_line orig_dir proj args =
       error "Output file must be in the current directory";
     if proj.makefile <> None then
       error "Option -o given more than once";
-    aux { proj with makefile = Some file } r  
+    aux { proj with makefile = Some file } r
   | v :: "=" :: def :: r ->
     aux { proj with defs = proj.defs @ [sourced (v,def)] } r
   | "-arg" :: a :: r ->
diff --git a/lib/envars.ml b/lib/envars.ml
index be82bfe9..3ee0c710 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -110,6 +110,7 @@ let check_file_else ~dir ~file oth =
   if Sys.file_exists (path / file) then path else oth ()
 
 let guess_coqlib fail =
+  getenv_else "COQLIB" (fun () ->
   let prelude = "theories/Init/Prelude.vo" in
   check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude
     (fun () ->
@@ -117,6 +118,7 @@ let guess_coqlib fail =
       then Coq_config.coqlib
       else
         fail "cannot guess a path for Coq libraries; please use -coqlib option")
+  )
 
 (** coqlib is now computed once during coqtop initialization *)
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 8491873e..458186b7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -57,10 +57,7 @@ let in_toplevel = ref false
 
 let profile = false
 
-let ide_slave = ref false
-
 let raw_print = ref false
-let univ_print = ref false
 
 let we_are_parsing = ref false
 
@@ -69,25 +66,25 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_6 | V8_7 | Current
+type compat_version = V8_7 | V8_8 | Current
 
 let compat_version = ref Current
 
 let version_compare v1 v2 = match v1, v2 with
-  | V8_6, V8_6 -> 0
-  | V8_6, _ -> -1
-  | _, V8_6 -> 1
   | V8_7, V8_7 -> 0
   | V8_7, _ -> -1
   | _, V8_7 -> 1
+  | V8_8, V8_8 -> 0
+  | V8_8, _ -> -1
+  | _, V8_8 -> 1
   | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
-  | V8_6 -> "8.6"
   | V8_7 -> "8.7"
+  | V8_8 -> "8.8"
   | Current -> "current"
 
 (* Translate *)
@@ -160,11 +157,3 @@ let print_mod_uid = ref false
 
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
-
-let dump_bytecode = ref false
-let set_dump_bytecode = (:=) dump_bytecode
-let get_dump_bytecode () = !dump_bytecode
-
-let dump_lambda = ref false
-let set_dump_lambda = (:=) dump_lambda
-let get_dump_lambda () = !dump_lambda
diff --git a/lib/flags.mli b/lib/flags.mli
index 85aaf879..9562e8fc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -10,6 +10,25 @@
 
 (** Global options of the system. *)
 
+(** WARNING: don't add new entries to this file!
+
+    This file is own its way to deprecation in favor of a purely
+   functional state, but meanwhile it will contain options that are
+   truly global to the system such as [compat] or [debug]
+
+    If you are thinking about adding a global flag, well, just
+   don't. First of all, options make testins exponentially more
+   expensive, due to the growth of flag combinations. So please make
+   some effort in order for your idea to work in a configuration-free
+   manner.
+
+    If you absolutely must pass an option to your new system, then do
+   so as a functional argument so flags are exposed to unit
+   testing. Then, register such parameters with the proper
+   state-handling mechanism of the top-level subsystem of Coq.
+
+ *)
+
 (** Command-line flags  *)
 
 val boot : bool ref
@@ -33,19 +52,13 @@ val in_toplevel : bool ref
 
 val profile : bool
 
-(* -ide_slave: printing will be more verbose, will affect stm caching *)
-val ide_slave : bool ref
-
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref
 
-(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
-val univ_print : bool ref
-
-type compat_version = V8_6 | V8_7 | Current
+type compat_version = V8_7 | V8_8 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
@@ -129,13 +142,3 @@ val print_mod_uid : bool ref
 
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
-
-(** Dump the bytecode after compilation (for debugging purposes) *)
-val dump_bytecode : bool ref
-val set_dump_bytecode : bool -> unit
-val get_dump_bytecode : unit -> bool
-
-(** Dump the VM lambda code after compilation (for debugging purposes) *)
-val dump_lambda : bool ref
-val set_dump_lambda : bool -> unit
-val get_dump_lambda : unit -> bool
diff --git a/lib/future.ml b/lib/future.ml
index 7a5b6f69..b372bedc 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -49,7 +49,7 @@ end
 module UUIDMap = Map.Make(UUID)
 module UUIDSet = Set.Make(UUID)
 
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 
 (* Val is not necessarily a final state, so the
    computation restarts from the state stocked into Val *)
@@ -103,7 +103,7 @@ let from_here ?(fix_exn=id) v = create fix_exn (Val v)
 let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
 
 let create_delegate ?(blocking=true) ~name fix_exn =
-  let assignement signal ck = fun v ->
+  let assignment signal ck = fun v ->
     let _, _, fix_exn, c = get ck in
     assert (match !c with Delegated _ -> true | _ -> false);
     begin match v with
@@ -118,7 +118,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
     (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
     (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
   let ck = create ~name fix_exn (Delegated wait) in
-  ck, assignement signal ck
+  ck, assignment signal ck
 
 (* TODO: get rid of try/catch to be stackless *)
 let rec compute ck : 'a value =
diff --git a/lib/future.mli b/lib/future.mli
index d9e8c87b..55f05518 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -70,10 +70,10 @@ val fix_exn_of : 'a computation -> fix_exn
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
    delegate assigns it. *)
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
   ?blocking:bool -> name:string ->
-  fix_exn -> 'a computation * ('a assignement -> unit)
+  fix_exn -> 'a computation * ('a assignment -> unit)
 
 (* Given a computation that is_exn, replace it by another one *)
 val replace : 'a computation -> 'a computation -> unit
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 08918594..41b3622a 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -6,6 +6,7 @@ Control
 Util
 
 Pp
+Pp_diff
 Stateid
 Loc
 Feedback
diff --git a/lib/pp.ml b/lib/pp.ml
index cd81f6e7..7f132686 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -139,7 +139,7 @@ let v   n s = Ppcmd_box(Pp_vbox n,s)
 let hv  n s = Ppcmd_box(Pp_hvbox n,s)
 let hov n s = Ppcmd_box(Pp_hovbox n,s)
 
-(* Opening and closed of tags *)
+(* Opening and closing of tags *)
 let tag t s = Ppcmd_tag(t,s)
 
 (* In new syntax only double quote char is escaped by repeating it *)
@@ -167,6 +167,20 @@ let rec pr_com ft s =
       Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
     | None -> ()
 
+let start_pfx = "start."
+let end_pfx = "end."
+
+let split_pfx pfx str =
+  let (str_len, pfx_len) = (String.length str, String.length pfx) in
+  if str_len >= pfx_len && (String.sub str 0 pfx_len) = pfx then
+    (pfx, String.sub str pfx_len (str_len - pfx_len)) else ("", str);;
+
+let split_tag tag =
+  let (pfx, ttag) = split_pfx start_pfx tag in
+  if pfx <> "" then (pfx, ttag) else
+    let (pfx, ttag) = split_pfx end_pfx tag in
+    (pfx, ttag);;
+
 (* pretty printing functions *)
 let pp_with ft pp =
   let cpp_open_box = function
@@ -297,3 +311,62 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 let prvect elem v = prvect_with_sep mt elem v
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
+
+(*** DEBUG code ***)
+
+let db_print_pp fmt pp =
+  let open Format in
+  let block_type fmt btype =
+    let (bt, v) =
+      match btype with
+      | Pp_hbox v -> ("Pp_hbox", v)
+      | Pp_vbox v -> ("Pp_vbox", v)
+      | Pp_hvbox v -> ("Pp_hvbox", v)
+      | Pp_hovbox v -> ("Pp_hovbox", v)
+    in
+    fprintf fmt "%s %d" bt v
+  in
+  let rec db_print_pp_r indent pp =
+    let ind () = fprintf fmt "%s" (String.make (2 * indent) ' ') in
+    ind();
+    match pp with
+    | Ppcmd_empty ->
+        fprintf fmt "Ppcmd_empty@;"
+    | Ppcmd_string str ->
+        fprintf fmt "Ppcmd_string '%s'@;" str
+    | Ppcmd_glue list ->
+        fprintf fmt "Ppcmd_glue@;";
+        List.iter (fun x -> db_print_pp_r (indent + 1) (repr x)) list;
+    | Ppcmd_box (block, pp) ->
+        fprintf fmt "Ppcmd_box %a@;" block_type block;
+        db_print_pp_r (indent + 1) (repr pp);
+    | Ppcmd_tag (tag, pp) ->
+        fprintf fmt "Ppcmd_tag %s@;" tag;
+        db_print_pp_r (indent + 1) (repr pp);
+    | Ppcmd_print_break (i, j) ->
+        fprintf fmt "Ppcmd_print_break %d %d@;" i j
+    | Ppcmd_force_newline ->
+        fprintf fmt "Ppcmd_force_newline@;"
+    | Ppcmd_comment list ->
+        fprintf fmt "Ppcmd_comment@;";
+        List.iter (fun x -> ind(); (fprintf fmt "%s@;" x)) list
+  in
+  pp_open_vbox fmt 0;
+  db_print_pp_r 0 pp;
+  pp_close_box fmt ();
+  pp_print_flush fmt ()
+
+let db_string_of_pp pp =
+  Format.asprintf "%a" db_print_pp pp
+
+let rec flatten pp =
+  match pp with
+  | Ppcmd_glue l -> Ppcmd_glue (List.concat (List.map
+      (fun x -> let x = flatten x in
+                  match x with
+                  | Ppcmd_glue l2 -> l2
+                  | p -> [p])
+      l))
+  | Ppcmd_box (block, pp) -> Ppcmd_box (block, flatten pp)
+  | Ppcmd_tag (tag, pp) -> Ppcmd_tag (tag, flatten pp)
+  | p -> p
diff --git a/lib/pp.mli b/lib/pp.mli
index f3a0a29b..ed31daa5 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -189,3 +189,22 @@ val pr_vertical_list : ('b -> t) -> 'b list -> t
 val pp_with          : Format.formatter -> t -> unit
 
 val string_of_ppcmds : t -> string
+
+
+(** Tag prefix to start a multi-token diff span *)
+val start_pfx : string
+
+(** Tag prefix to end a multi-token diff span *)
+val end_pfx : string
+
+(** Split a tag into prefix and base tag *)
+val split_tag : string -> string * string
+
+(** Print the Pp in tree form for debugging *)
+val db_print_pp : Format.formatter -> t -> unit
+
+(** Print the Pp in tree form for debugging, return as a string *)
+val db_string_of_pp : t -> string
+
+(** Combine nested Ppcmd_glues *)
+val flatten : t -> t
diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml
new file mode 100644
index 00000000..7b4b1eab
--- /dev/null
+++ b/lib/pp_diff.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* DEBUG/UNIT TEST *)
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let log_out_ch = ref stdout
+let cprintf s = cfprintf !log_out_ch s
+
+
+module StringDiff = Diff2.Make(struct
+  type elem = String.t
+  type t = elem array
+  let get t i = Array.get t i
+  let length t = Array.length t
+end)
+
+type diff_type =
+  [ `Removed
+  | `Added
+  | `Common
+  ]
+
+type diff_list = StringDiff.elem Diff2.edit list
+
+(* debug print diff data structure *)
+let db_print_diffs fmt diffs =
+  let open Format in
+  let print_diff = function
+    | `Common (opos, npos, s) ->
+      fprintf fmt "Common '%s' opos = %d npos = %d\n" s opos npos;
+    | `Removed (pos, s) ->
+      fprintf fmt "Removed '%s' opos = %d\n" s pos;
+    | `Added (pos, s) ->
+      fprintf fmt "Added '%s' npos = %d\n" s pos;
+  in
+  pp_open_vbox fmt 0;
+  List.iter print_diff diffs;
+  pp_close_box fmt ();
+  pp_print_flush fmt ()
+
+let string_of_diffs diffs =
+  Format.asprintf "%a" db_print_diffs diffs
+
+(* Adjust the diffs returned by the Myers algorithm to reduce the span of the
+changes.  This gives more natural-looking diffs.
+
+While the Myers algorithm minimizes the number of changes between two
+sequences, it doesn't minimize the span of the changes.  For example,
+representing elements in common in lower case and inserted elements in upper
+case (but ignoring case in the algorithm), ABabC and abABC both have 3 changes
+(A, B and C).  However the span of the first sequence is 5 elements (ABabC)
+while the span of the second is 3 elements (ABC).
+
+The algorithm modifies the changes iteratively, for example ABabC -> aBAbC -> abABC
+
+dtype: identifies which of Added OR Removed to use; the other one is ignored.
+diff_list: output from the Myers algorithm
+*)
+let shorten_diff_span dtype diff_list =
+  let changed = ref false in
+  let diffs = Array.of_list diff_list in
+  let len = Array.length diffs in
+  let vinfo index =
+    match diffs.(index) with
+    | `Common (opos, npos, s) -> (`Common, opos, npos, s)
+    | `Removed (pos, s) -> (`Removed, pos, 0, s)
+    | `Added (pos, s) -> (`Added, 0, pos, s) in
+  let get_variant index =
+    let (v, _, _, _) = vinfo index in
+    v in
+  let get_str index =
+    let (_, _, _, s) = vinfo index in
+    s in
+
+  let iter start len lt incr = begin
+    let src = ref start in
+    let dst = ref start in
+    while (lt !src len) do
+      if (get_variant !src) = dtype then begin
+        if (lt !dst !src) then
+          dst := !src;
+        while (lt !dst len) && (get_variant !dst) <> `Common do
+          dst := !dst + incr;
+        done;
+        if (lt !dst len) && (get_str !src) = (get_str !dst) then begin
+          (* swap diff *)
+          let (_, c_opos, c_npos, str) = vinfo !dst
+          and (_, v_opos, v_npos, _) = vinfo !src in
+          changed := true;
+          if dtype = `Added then begin
+            diffs.(!src) <- `Common (c_opos, v_npos, str);
+            diffs.(!dst) <- `Added (c_npos, str);
+          end else begin
+            diffs.(!src) <- `Common (v_opos, c_npos, str);
+            diffs.(!dst) <- `Removed (c_opos, str)
+          end
+        end
+      end;
+      src := !src + incr
+    done
+  end in
+
+  iter 0 len (<) 1; (* left to right *)
+  iter (len-1) (-1) (>) (-1); (* right to left *)
+  if !changed then Array.to_list diffs else diff_list;;
+
+let has_changes diffs =
+  let rec has_changes_r diffs added removed =
+    match diffs with
+    | `Added _ :: t   -> has_changes_r t true removed
+    | `Removed _ :: t -> has_changes_r t added true
+    | h :: t -> has_changes_r t added removed
+    | [] -> (added, removed) in
+  has_changes_r diffs false false;;
+
+(* get the Myers diff of 2 lists of strings *)
+let diff_strs old_strs new_strs =
+  let diffs = List.rev (StringDiff.diff old_strs new_strs) in
+  shorten_diff_span `Removed (shorten_diff_span `Added diffs);;
+
+(* Default string tokenizer.  Makes each character a separate strin.
+Whitespace is not ignored.  Doesn't handle UTF-8 differences well. *)
+let def_tokenize_string s =
+  let limit = (String.length s) - 1 in
+  let strs : string list ref = ref [] in
+  for i = 0 to limit do
+    strs := (String.make 1 s.[i]) :: !strs
+  done;
+  List.rev !strs
+
+(* get the Myers diff of 2 strings *)
+let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str =
+  let old_toks = Array.of_list (tokenize_string old_str)
+  and new_toks = Array.of_list (tokenize_string new_str) in
+  diff_strs old_toks new_toks;;
+
+let get_dinfo = function
+  | `Common (_, _, s) -> (`Common, s)
+  | `Removed (_, s) -> (`Removed, s)
+  | `Added (_, s) -> (`Added, s)
+
+[@@@ocaml.warning "-32"]
+let string_of_diff_type = function
+  | `Common  -> "Common"
+  | `Removed -> "Removed"
+  | `Added -> "Added"
+[@@@ocaml.warning "+32"]
+
+let wrap_in_bg diff_tag pp =
+  let open Pp in
+  (tag (Pp.start_pfx ^ diff_tag ^ ".bg") (str "")) ++ pp ++
+  (tag (Pp.end_pfx   ^ diff_tag ^ ".bg") (str ""))
+
+exception Diff_Failure of string
+
+let add_diff_tags which pp diffs  =
+  let open Pp in
+  let diff_tag = if which = `Added then "diff.added" else "diff.removed" in
+  let diffs : diff_list ref = ref diffs in
+  let in_diff = ref false in (* true = buf chars need a tag *)
+  let in_span = ref false in (* true = last pp had a start tag *)
+  let trans = ref false in   (* true = this diff starts/ends highlight *)
+  let buf = Buffer.create 16 in
+  let acc_pp = ref [] in
+  let diff_str, diff_ind, diff_len = ref "", ref 0, ref 0 in
+  let prev_dtype, dtype, next_dtype = ref `Common, ref `Common, ref `Common in
+  let is_white c = List.mem c [' '; '\t'; '\n'; '\r'] in
+
+  let skip () =
+    while !diffs <> [] &&
+      (let (t, _) = get_dinfo (List.hd !diffs) in
+        t <> `Common && t <> which)
+    do
+      diffs := List.tl !diffs
+    done
+  in
+
+  let put_tagged case =
+    if Buffer.length buf > 0 then begin
+      let pp = str (Buffer.contents buf) in
+      Buffer.clear buf;
+      let tagged = match case with
+      | ""      -> pp
+      | "tag"   -> tag diff_tag pp
+      | "start" -> in_span := true;  tag (start_pfx ^ diff_tag) pp
+      | "end"   -> in_span := false; tag (end_pfx ^ diff_tag) pp
+      | _ -> raise (Diff_Failure "invalid tag id in put_tagged, should be impossible") in
+      acc_pp := tagged :: !acc_pp
+    end
+  in
+
+  let output_pps () =
+    let next_diff_char_hl = if !diff_ind < !diff_len then !dtype = which else !next_dtype = which in
+    let tag = if not !in_diff then ""
+              else  if !in_span then
+                      if next_diff_char_hl then "" else "end"
+                    else
+                      if next_diff_char_hl then "start" else "tag" in
+    put_tagged tag;  (* flush any remainder *)
+    let l = !acc_pp in
+    acc_pp := [];
+    match List.length l with
+    | 0 -> str ""
+    | 1 -> List.hd l
+    | _ -> seq (List.rev l)
+  in
+
+  let maybe_next_diff () =
+    if !diff_ind = !diff_len && (skip(); !diffs <> []) then begin
+      let (t, s) = get_dinfo (List.hd !diffs) in
+      diff_str := s; diff_ind := 0; diff_len := String.length !diff_str;
+      diffs := List.tl !diffs; skip();
+      prev_dtype := !dtype;
+      dtype := t;
+      next_dtype := (match !diffs with
+        | diff2 :: _ -> let (nt, _) = get_dinfo diff2 in nt
+        | [] -> `Common);
+      trans := !dtype <> !prev_dtype
+    end;
+  in
+
+  let s_char c =
+    maybe_next_diff ();
+    (* matching first should handle tokens with spaces, e.g. in comments/strings *)
+    if !diff_ind < !diff_len && c = !diff_str.[!diff_ind] then begin
+      if !dtype = which && !trans && !diff_ind = 0 then begin
+        put_tagged "";
+        in_diff := true
+      end;
+      Buffer.add_char buf c;
+      diff_ind := !diff_ind + 1;
+      if !dtype = which && !dtype <> !next_dtype && !diff_ind = !diff_len then begin
+        put_tagged (if !in_span then "end" else "tag");
+        in_diff := false
+      end
+    end else if is_white c then
+      Buffer.add_char buf c
+    else begin
+      cprintf "mismatch: expected '%c' but got '%c'\n" !diff_str.[!diff_ind] c;
+      raise (Diff_Failure "string mismatch, shouldn't happen")
+    end
+  in
+
+  (* rearrange so existing tags are inside diff tags, provided that those tags
+    only contain Ppcmd_string's.  Other cases (e.g. tag of a box) are not supported. *)
+  (* todo: Is there a better way to do this in OCaml without multiple 'repr's? *)
+  let reorder_tags child pp_tag pp =
+    match repr child with
+    | Ppcmd_tag (t1, pp) -> tag t1 (tag pp_tag pp)
+    | Ppcmd_glue l ->
+      if List.exists (fun x ->
+          match repr x with
+          | Ppcmd_tag (_, _) -> true
+          | _ -> false)  l
+      then seq (List.map (fun x ->
+          match repr x with
+          | Ppcmd_tag (t2, pp2) -> tag t2 (tag pp_tag pp2)
+          | pp2 -> tag pp_tag (unrepr pp2))   l)
+      else child
+    | _ -> tag pp_tag child
+  in
+
+  let rec add_tags_r pp =
+    let r_pp = repr pp in
+    match r_pp with
+    | Ppcmd_string s -> String.iter s_char s; output_pps ()
+    | Ppcmd_glue l -> seq (List.map add_tags_r l)
+    | Ppcmd_box (block_type, pp) -> unrepr (Ppcmd_box (block_type, add_tags_r pp))
+    | Ppcmd_tag (pp_tag, pp) -> reorder_tags (add_tags_r pp) pp_tag pp
+    | _ -> pp
+  in
+  let (has_added, has_removed) = has_changes !diffs in
+  let rv = add_tags_r pp in
+  skip ();
+  if !diffs <> [] then
+    raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible");
+  if has_added || has_removed then wrap_in_bg diff_tag rv else rv;;
+
+let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp =
+  let open Pp in
+  let o_str = string_of_ppcmds o_pp in
+  let n_str = string_of_ppcmds n_pp in
+  let diffs = diff_str ~tokenize_string o_str n_str in
+  (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);;
+
+let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp =
+  let open Pp in
+  let o_str = string_of_ppcmds o_pp in
+  let n_str = string_of_ppcmds n_pp in
+  let diffs = diff_str ~tokenize_string o_str n_str in
+  let (_, has_removed) = has_changes diffs in
+  let added = add_diff_tags `Added n_pp diffs in
+  if show_removed && has_removed then
+    let removed = add_diff_tags `Removed o_pp diffs in
+    (v 0 (removed ++ cut() ++ added))
+  else added;;
diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli
new file mode 100644
index 00000000..03468271
--- /dev/null
+++ b/lib/pp_diff.mli
@@ -0,0 +1,116 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(**
+Computes the differences between 2 Pp's and adds additional tags to a Pp
+to highlight them.  Strings are split into tokens using the Coq lexer,
+then the lists of tokens are diffed using the Myers algorithm.  A fixup routine,
+shorten_diff_span, shortens the span of the diff result in some cases.
+
+Highlights use 4 tags to specify the color and underline/strikeout.  These are
+"diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg".  The
+first two are for added or removed text; the last two are for unmodified parts
+of a modified item.  Diffs that span multiple strings in the Pp are tagged with
+"start.diff.*" and "end.diff.*", but only on the first and last strings of the span.
+
+If the inputs are not acceptable to the lexer, break the strings into
+lists of tokens and call diff_strs, then add_diff_tags with a Pp.t that matches
+the input lists of strings.  Tokens that the lexer doesn't return exactly as they
+appeared in the input will raise an exception in add_diff_tags (e.g. comments
+and quoted strings).  Fixing that requires tweaking the lexer.
+
+Limitations/Possible enhancements:
+
+- Make diff_pp immune to unlexable strings by adding a flag to the lexer.
+*)
+
+(** Compute the diff between two Pp.t structures and return
+versions of each with diffs highlighted as (old, new) *)
+val diff_pp : ?tokenize_string:(string -> string list) -> Pp.t -> Pp.t -> Pp.t * Pp.t
+
+(** Compute the diff between two Pp.t structures and return
+a highlighted Pp.t.  If [show_removed] is true, show separate lines for
+removals and additions, otherwise only show additions *)
+val diff_pp_combined : ?tokenize_string:(string -> string list) -> ?show_removed:bool -> Pp.t -> Pp.t -> Pp.t
+
+(** Raised if the diff fails *)
+exception Diff_Failure of string
+
+module StringDiff :
+sig
+  type elem = String.t
+  type t = elem array
+end
+
+type diff_type =
+  [ `Removed
+  | `Added
+  | `Common
+  ]
+
+type diff_list = StringDiff.elem Diff2.edit list
+
+(** Compute the difference between 2 strings in terms of tokens, using the
+lexer to identify tokens.
+
+If the strings are not lexable, this routine will raise Diff_Failure.
+(I expect to modify the lexer soon so this won't happen.)
+
+Therefore you should catch any exceptions.  The workaround for now is for the
+caller to tokenize the strings itself and then call diff_strs.
+*)
+val diff_str : ?tokenize_string:(string -> string list) -> string -> string -> StringDiff.elem Diff2.edit list
+
+(** Compute the differences between 2 lists of strings, treating the strings
+in the lists as indivisible units.
+*)
+val diff_strs : StringDiff.t -> StringDiff.t -> StringDiff.elem Diff2.edit list
+
+(** Generate a new Pp that adds tags marking diffs to a Pp structure:
+which: either `Added or `Removed, indicates which type of diffs to add
+pp: the original structure. For `Added, must be the new pp passed to diff_pp
+  For `Removed, must be the old pp passed to diff_pp.  Passing the wrong one
+  will likely raise Diff_Failure.
+diffs: the diff list returned by diff_pp
+
+Diffs of single strings in the Pp are tagged with "diff.added" or "diff.removed".
+Diffs that span multiple strings in the Pp are tagged with "start.diff.*" or
+"end.diff.*", but only on the first and last strings of the span.
+
+Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends
+in the middle of the string.  Whitespace just before or just after a diff will
+not be part of the highlight.
+
+Prexisting tags in pp may contain only a single Ppcmd_string.  Those tags will be
+placed inside the diff tags to ensure proper nesting of tags within spans of
+"start.diff.*" ... "end.diff.*".
+
+Under some  "impossible" conditions, this routine may raise Diff_Failure.
+If you want to make your call especially bulletproof, catch this
+exception, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val add_diff_tags : diff_type -> Pp.t -> StringDiff.elem Diff2.edit list -> Pp.t
+
+(** Returns a boolean pair (added, removed) for [diffs] where a true value
+indicates that something was added/removed in the diffs.
+*)
+val has_changes : diff_list -> bool * bool
+
+val get_dinfo : StringDiff.elem Diff2.edit -> diff_type * string
+
+(** Returns a modified [pp] with the background highlighted with
+"start.<diff_tag>.bg" and "end.<diff_tag>.bg" tags at the beginning
+and end of the returned Pp.t
+*)
+val wrap_in_bg : string -> Pp.t -> Pp.t
+
+(** Displays the diffs to a printable format for debugging *)
+val string_of_diffs : diff_list -> string
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 0e371025..e1c6a4c4 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -94,22 +94,28 @@ let is_node t =
       Node _ -> true
     | _ -> false
 
-
 let rec map f t = match t with
     Param(i,j) -> Param(i,j)
   | Node (a,sons) -> Node (f a, Array.map (map f) sons)
   | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
 
-let smartmap f t = match t with
-    Param _ -> t
-  | Node (a,sons) ->
-      let a'=f a and sons' = Array.smartmap (map f) sons in
-      if a'==a && sons'==sons then t
-      else Node (a',sons')
-  | Rec(j,defs) ->
-      let defs' = Array.smartmap (map f) defs in
-      if defs'==defs then t
-      else Rec(j,defs')
+module Smart =
+struct
+
+  let map f t = match t with
+      Param _ -> t
+    | Node (a,sons) ->
+        let a'=f a and sons' = Array.Smart.map (map f) sons in
+        if a'==a && sons'==sons then t
+        else Node (a',sons')
+    | Rec(j,defs) ->
+        let defs' = Array.Smart.map (map f) defs in
+        if defs'==defs then t
+        else Rec(j,defs')
+
+end
+
+let smartmap = Smart.map
 
 (** Structural equality test, parametrized by an equality on elements *)
 
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 8edfc3d3..5ab14f60 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -74,13 +74,22 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -
 
 (** Iterators *)
 
+(** See also [Smart.map] *)
 val map : ('a -> 'b) -> 'a t -> 'b t
 
-(** [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
 val smartmap : ('a -> 'a) -> 'a t -> 'a t
+(** @deprecated Same as [Smart.map] *)
 
 (** A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t
 
 val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 (** @deprecated Same as [Rtree.equal] *)
+
+module Smart :
+sig
+
+  (** [(Smart.map f t) == t] if [(f a) ==a ] for all nodes *)
+  val map : ('a -> 'a) -> 'a t -> 'a t
+
+end
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 63e9e452..0652623b 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -15,14 +15,12 @@ let accept_timeout = 10.0
 let pr_err s = Printf.eprintf "(Spawn  ,%d) %s\n%!" (Unix.getpid ()) s
 let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
 
-type req = ReqDie | ReqStats | Hello of int * int
-type resp = RespStats of Gc.stat
+type req = ReqDie | Hello of int * int
 
 module type Control = sig
   type handle
 
   val kill : handle -> unit
-  val stats : handle -> Gc.stat
   val wait : handle -> Unix.process_status
   val unixpid : handle -> int
   val uid : handle -> string
@@ -43,7 +41,6 @@ module type MainLoopModel = sig
 end
 
 (* Common code *)
-let assert_ b s = if not b then CErrors.anomaly (Pp.str s)
 
 (* According to http://caml.inria.fr/mantis/view.php?id=5325
  * you can't use the same socket for both writing and reading (may change
@@ -125,14 +122,26 @@ let filter_args args =
   Array.of_list (aux (Array.to_list args))
 
 let spawn_with_control prefer_sock env prog args =
-  let control_sock, control_sock_name = mk_socket_channel () in
-  let extra = [| "-control-channel"; control_sock_name |] in
-  let args = Array.append extra (filter_args args) in
+  (* on non-Unix systems we create a control channel *)
+  let not_Unix = Sys.os_type <> "Unix" in
+  let args = filter_args args in
+  let args, control_sock =
+    if not_Unix then
+      let control_sock, control_sock_name = mk_socket_channel () in
+      let extra = [| "-control-channel"; control_sock_name |] in
+      Array.append extra args, Some control_sock
+    else
+      args, None in
   let (pid, cin, cout, s), is_sock =
-    if Sys.os_type <> "Unix" || prefer_sock
+    if not_Unix (* pipes only work well on Unix *) || prefer_sock
     then spawn_sock env prog args, true
     else spawn_pipe env prog args, false in
-  let _, oob_resp, oob_req = accept control_sock in
+  let oob_resp, oob_req =
+    if not_Unix then
+      let _, oob_resp, oob_req = accept (Option.get control_sock) in
+      Some oob_resp, Some oob_req
+    else
+      None, None in
   pid, oob_resp, oob_req, cin, cout, s, is_sock
 
 let output_death_sentence pid oob_req =
@@ -146,8 +155,8 @@ module Async(ML : MainLoopModel) = struct
 type process = {
   cin  : in_channel;
   cout : out_channel;
-  oob_resp : in_channel;
-  oob_req  : out_channel;
+  oob_resp : in_channel option;
+  oob_req  : out_channel option;
   gchan : ML.async_chan;
   pid : int;
   mutable watch : ML.watch_id option;
@@ -166,11 +175,11 @@ let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) =
   if not alive then prerr_endline "This process is already dead"
   else begin try
     Option.iter ML.remove_watch watch;
-    output_death_sentence (uid p) oob_req;
+    Option.iter (output_death_sentence (uid p)) oob_req;
     close_in_noerr cin;
     close_out_noerr cout;
-    close_in_noerr oob_resp;
-    close_out_noerr oob_req;
+    Option.iter close_in_noerr oob_resp;
+    Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid 9;
     p.watch <- None
   with e -> prerr_endline ("kill: "^Printexc.to_string e) end
@@ -199,12 +208,6 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
   );
   p, cout
 
-let stats { oob_req; oob_resp; alive } =
-  assert_ alive "This process is dead.";
-  output_value oob_req ReqStats;
-  flush oob_req;
-  input_value oob_resp
-
 let rec wait p =
   (* On windows kill is not reliable, so wait may never return. *) 
   if Sys.os_type = "Unix" then 
@@ -221,8 +224,8 @@ module Sync () = struct
 type process = {
   cin  : in_channel;
   cout : out_channel;
-  oob_resp : in_channel;
-  oob_req  : out_channel;
+  oob_resp : in_channel option;
+  oob_req  : out_channel option;
   pid : int;
   mutable alive : bool;
 }
@@ -242,20 +245,14 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
   p.alive <- false;
   if not alive then prerr_endline "This process is already dead"
   else begin try
-    output_death_sentence (uid p) oob_req;
+    Option.iter (output_death_sentence (uid p)) oob_req;
     close_in_noerr cin;
     close_out_noerr cout;
-    close_in_noerr oob_resp;
-    close_out_noerr oob_req;
+    Option.iter close_in_noerr oob_resp;
+    Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid 9;
   with e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
-let stats { oob_req; oob_resp; alive } =
-  assert_ alive "This process is dead.";
-  output_value oob_req ReqStats;
-  flush oob_req;
-  let RespStats g = input_value oob_resp in g
-
 let rec wait p =
   (* On windows kill is not reliable, so wait may never return. *) 
   if Sys.os_type = "Unix" then 
diff --git a/lib/spawn.mli b/lib/spawn.mli
index c7a56349..944aa27a 100644
--- a/lib/spawn.mli
+++ b/lib/spawn.mli
@@ -25,7 +25,6 @@ module type Control = sig
   type handle
 
   val kill : handle -> unit
-  val stats : handle -> Gc.stat
   val wait : handle -> Unix.process_status
   val unixpid : handle -> int
   
@@ -76,6 +75,5 @@ end
 
 (* This is exported to separate the Spawned module, that for simplicity assumes
  * Threads so it is in a separate file *)
-type req = ReqDie | ReqStats | Hello of int * int
+type req = ReqDie | Hello of int * int
 val proto_version : int
-type resp = RespStats of Gc.stat
diff --git a/lib/stateid.ml b/lib/stateid.ml
index a258d505..5485c4bf 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -11,15 +11,11 @@
 type t = int
 let initial = 1
 let dummy = 0
-let fresh, in_range =
+let fresh =
   let cur = ref initial in
-  (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
+  fun () -> incr cur; !cur
 let to_string = string_of_int
-let of_int id =
-  (* Coqide too to parse ids too, but cannot check if they are valid.
-   * Hence we check for validity only if we are an ide slave. *)
-  if !Flags.ide_slave then assert (in_range id);
-  id
+let of_int id = id
 let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
diff --git a/lib/system.ml b/lib/system.ml
index dfede29e..4bc56beb 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -83,7 +83,9 @@ let file_exists_respecting_case path f =
   let rec aux f =
     let bf = Filename.basename f in
     let df = Filename.dirname f in
-    (String.equal df "." || aux df)
+    (* When [df] is the same as [f], it means that the root of the file system
+       has been reached. There is no point in looking further up. *)
+    (String.equal df "." || String.equal f df || aux df)
     && exists_in_dir_respecting_case (Filename.concat path df) bf
   in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f
 
@@ -116,18 +118,6 @@ let where_in_path ?(warn=true) path filename =
     let f = Filename.concat lpe filename in
     if file_exists_respecting_case lpe filename then [lpe,f] else []))
 
-let where_in_path_rex path rex =
-  search path (fun lpe ->
-    try
-      let files = Sys.readdir lpe in
-      CList.map_filter (fun name ->
-        try
-          ignore(Str.search_forward rex name 0);
-          Some (lpe,Filename.concat lpe name)
-        with Not_found -> None)
-      (Array.to_list files)
-    with Sys_error _ -> [])
-
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
     (* the name is considered to be a physical name and we use the file
@@ -312,3 +302,9 @@ let with_time ~batch f x =
     let msg2 = if batch then "" else " (failure)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
+
+let get_toplevel_path top =
+  let dir = Filename.dirname Sys.executable_name in
+  let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
+  let eff = if Dynlink.is_native then ".opt" else ".byte" in
+  dir ^ Filename.dir_sep ^ top ^ eff ^ exe
diff --git a/lib/system.mli b/lib/system.mli
index 3349dfea..a3428003 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -50,8 +50,6 @@ val is_in_path : CUnix.load_path -> string -> bool
 val is_in_system_path : string -> bool
 val where_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
-val where_in_path_rex :
-  CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
 
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
@@ -107,3 +105,21 @@ val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.t
 
 val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
+
+(** [get_toplevel_path program] builds a complete path to the
+   executable denoted by [program]. This involves:
+
+   - locating the directory: we don't rely on PATH as to make calls to
+   /foo/bin/coqtop chose the right /foo/bin/coqproofworker
+
+   - adding the proper suffixes: .opt/.byte depending on the current
+   mode, + .exe if in windows.
+
+ Note that this function doesn't check that the executable actually
+ exists. This is left back to caller, as well as the choice of
+ fallback strategy. We could add a fallback strategy here but it is
+ better not to as in most cases if this function fails to construct
+ the right name you want you execution to fail rather than fall into
+ choosing some random binary from the system-wide installation of
+ Coq. *)
+val get_toplevel_path : string -> string
diff --git a/lib/util.ml b/lib/util.ml
index 7d7d380b..38d73d34 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -38,8 +38,8 @@ let is_blank = function
 
 module Empty =
 struct
-  type t
-  let abort (x : t) = assert false
+  type t = { abort : 'a. 'a }
+  let abort (x : t) = x.abort
 end
 
 (* Strings *)