34 files changed, 745 insertions, 275 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index 7d9c528e78..0f9476605b 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -55,7 +55,7 @@ let record_in_aux_at ?loc key v =
       match loc with
       | Some loc -> let i, j = Loc.unloc loc in
                     Printf.fprintf oc "%d %d %s %S\n" i j key v
-      | None     -> Printf.fprintf oc "--- %s %S\n" key v
+      | None     -> Printf.fprintf oc "0 0 %s %S\n" key v
     ) !oc
 
 let current_loc : Loc.t option ref = ref None
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 9750221143..811fcf4063 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 ec34dd62c5..4e2fe7621d 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 92c86eaea3..0cf989e494 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -22,11 +22,8 @@ type t = {
 let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
 
-let current_loc = ref None
 let flags = ref ""
 
-let set_current_loc loc = current_loc := loc
-
 let get_flags () = !flags
 
 let add_warning_in_category ~name ~category =
@@ -123,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
 
@@ -133,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 =
@@ -149,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
@@ -170,7 +167,6 @@ let create ~name ~category ?(default=Enabled) pp =
   set_flags !flags;
   fun ?loc x ->
            let w = Hashtbl.find warnings name in
-           let loc = Option.append loc !current_loc in
            match w.status with
            | Disabled -> ()
            | AsError -> CErrors.user_err ?loc (pp x)
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index fa96b18c8c..f97a53c4d7 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -10,8 +10,6 @@
 
 type status = Disabled | Enabled | AsError
 
-val set_current_loc : Loc.t option -> unit
-
 val create : name:string -> category:string -> ?default:status ->
              ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit
 
diff --git a/lib/control.ml b/lib/control.ml
index e67cd8b38d..3fbeb168c4 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -85,4 +85,7 @@ let timeout_fun = match Sys.os_type with
 | "Unix" | "Cygwin" -> { timeout = unix_timeout }
 | _ -> { timeout = windows_timeout }
 
-let timeout n f e = timeout_fun.timeout n f e
+let timeout_fun_ref = ref timeout_fun
+let set_timeout f = timeout_fun_ref := f
+
+let timeout n f e = !timeout_fun_ref.timeout n f e
diff --git a/lib/control.mli b/lib/control.mli
index 415e054625..59e2a15158 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -24,3 +24,8 @@ val check_for_interrupt : unit -> unit
 val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b
 (** [timeout n f x e] tries to compute [f x], and if it fails to do so
     before [n] seconds, it raises [e] instead. *)
+
+(** Set a particular timeout function; warning, this is an internal
+   API and it is scheduled to go away. *)
+type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }
+val set_timeout : timeout -> unit
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml
index d6c340f691..868042303d 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml
@@ -8,6 +8,10 @@
 (*         *     (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. *)
+
 type arg_source = CmdLine | ProjectFile
 
 type 'a sourced = { thing : 'a; source : arg_source }
@@ -21,6 +25,7 @@ type project = {
   v_files : string sourced list;
   mli_files : string sourced list;
   ml4_files : string sourced list;
+  mlg_files : string sourced list;
   ml_files : string sourced list;
   mllib_files : string sourced list;
   mlpack_files : string sourced list;
@@ -58,6 +63,7 @@ let mk_project project_file makefile install_kind use_ocamlopt = {
   v_files = [];
   mli_files = [];
   ml4_files = [];
+  mlg_files = [];
   ml_files = [];
   mllib_files = [];
   mlpack_files = [];
@@ -82,30 +88,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 *)
@@ -117,12 +143,12 @@ let exists_dir dir =
   try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
 
 
-let process_cmd_line orig_dir proj args =
+let process_cmd_line ~warning_fn orig_dir proj args =
   let parsing_project_file = ref (proj.project_file <> None) in
   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 +161,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_fn "-install set more than once.");
     let install = match d with
       | "user" -> UserInstall
       | "none" -> NoInstall
@@ -167,8 +193,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_fn "Multiple project files are deprecated."
     in
     parsing_project_file := true;
     let proj = aux { proj with project_file = Some file } (parse file) in
@@ -182,7 +207,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 ->
@@ -191,11 +216,12 @@ let process_cmd_line orig_dir proj args =
       let f = CUnix.correct_path f orig_dir in
       let proj =
         if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
-        else match CUnix.get_extension f with
+        else match Filename.extension f with
           | ".v" ->
             { proj with v_files = proj.v_files @ [sourced f] }
         | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
         | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] }
+        | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] }
         | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] }
         | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] }
         | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] }
@@ -206,11 +232,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) args
+let cmdline_args_to_project ~warning_fn ~curdir args =
+  process_cmd_line ~warning_fn curdir (mk_project None None None true) args
 
-let read_project_file f =
-  process_cmd_line (Filename.dirname f)
+let read_project_file ~warning_fn f =
+  process_cmd_line ~warning_fn (Filename.dirname f)
     (mk_project (Some f) None (Some NoInstall) true) (parse f)
 
 let rec find_project_file ~from ~projfile_name =
@@ -222,9 +248,9 @@ let rec find_project_file ~from ~projfile_name =
     else find_project_file ~from:newdir ~projfile_name
 ;;
 
-let all_files { v_files; ml_files; mli_files; ml4_files;
+let all_files { v_files; ml_files; mli_files; ml4_files; mlg_files;
                 mllib_files; mlpack_files } =
-  v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files
+  v_files @ mli_files @ ml4_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files
 
 let map_sourced_list f l = List.map (fun x -> f x.thing) l
 ;;
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 5780bb5d78..20b276ce8c 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -23,6 +23,7 @@ type project = {
   v_files : string sourced list;
   mli_files : string sourced list;
   ml4_files : string sourced list;
+  mlg_files : string sourced list;
   ml_files : string sourced list;
   mllib_files : string sourced list;
   mlpack_files : string sourced list;
@@ -50,8 +51,8 @@ and install =
   | TraditionalInstall
   | UserInstall
 
-val cmdline_args_to_project : curdir:string -> string list -> project
-val read_project_file : string -> project
+val cmdline_args_to_project : warning_fn:(string -> unit) -> curdir:string -> string list -> project
+val read_project_file : warning_fn:(string -> unit) -> string -> project
 val coqtop_args_from_project : project -> string list
 val find_project_file : from:string -> projfile_name:string -> string option
 
diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000000..232c208aa6
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1,7 @@
+(library
+ (name lib)
+ (synopsis "Coq's Utility Library [coq-specific]")
+ (public_name coq.lib)
+ (wrapped false)
+ (modules_without_implementation xml_datatype)
+ (libraries threads coq.clib coq.config))
diff --git a/lib/envars.ml b/lib/envars.ml
index be82bfe9bb..b5036e7340 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -34,22 +34,7 @@ let home ~warn =
 
 let path_to_list p =
   let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
-    String.split sep p
-
-let user_path () =
-  path_to_list (Sys.getenv "PATH") (* may raise Not_found *)
-
-(* Finding a name in path using the equality provided by the file system *)
-(* whether it is case-sensitive or case-insensitive *)
-let rec which l f =
-  match l with
-    | [] ->
-      raise Not_found
-    | p :: tl ->
-      if Sys.file_exists (p / f) then
-	p
-      else
-	which tl f
+    String.split_on_char sep p
 
 let expand_path_macros ~warn s =
   let rec expand_atom s i =
@@ -110,6 +95,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,15 +103,21 @@ let guess_coqlib fail =
       then Coq_config.coqlib
       else
         fail "cannot guess a path for Coq libraries; please use -coqlib option")
+  )
+
+let coqlib : string option ref = ref None
+let set_user_coqlib path = coqlib := Some path
 
 (** coqlib is now computed once during coqtop initialization *)
 
 let set_coqlib ~fail =
-  if not !Flags.coqlib_spec then
+  match !coqlib with
+  | Some _ -> ()
+  | None ->
     let lib = if !Flags.boot then coqroot else guess_coqlib fail in
-    Flags.coqlib := lib
+    coqlib := Some lib
 
-let coqlib () = !Flags.coqlib
+let coqlib () = Option.default "" !coqlib
 
 let docdir () =
   (* This assumes implicitly that the suffix is non-trivial *)
@@ -153,29 +145,8 @@ let coqpath =
 
 (** {2 Caml paths} *)
 
-let exe s = s ^ Coq_config.exec_extension
-
 let ocamlfind () = Coq_config.ocamlfind
 
-(** {2 Camlp5 paths} *)
-
-let guess_camlp5bin () = which (user_path ()) (exe "camlp5")
-
-let camlp5bin () =
-  if !Flags.boot then Coq_config.camlp5bin else
-    try guess_camlp5bin ()
-    with Not_found ->
-      Coq_config.camlp5bin
-
-let camlp5lib () =
-  if !Flags.boot then
-    Coq_config.camlp5lib
-  else
-    let ex, res = CUnix.run_command (ocamlfind () ^ " query camlp5") in
-    match ex with
-      | Unix.WEXITED 0 -> String.strip res
-      | _ -> "/dev/null"
-
 (** {1 XDG utilities} *)
 
 let xdg_data_home warn =
@@ -206,10 +177,6 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs =
   fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
   fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
   fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
-  fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o;
-  fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name (camlp5bin ());
-  fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name (camlp5lib ());
-  fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat;
   fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
   fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
     (if Coq_config.has_natdynlink then "true" else "false");
diff --git a/lib/envars.mli b/lib/envars.mli
index 66b86252c7..ebf86d0650 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -41,6 +41,9 @@ val configdir : unit -> string
 (** [set_coqlib] must be runned once before any access to [coqlib] *)
 val set_coqlib : fail:(string -> string) -> unit
 
+(** [set_user_coqlib path] sets the coqlib directory explicitedly. *)
+val set_user_coqlib : string -> unit
+
 (** [coqbin] is the name of the current executable. *)
 val coqbin : string
 
@@ -58,12 +61,6 @@ val coqpath : string list
 (** [camlfind ()] is the path to the ocamlfind binary. *)
 val ocamlfind : unit -> string
 
-(** [camlp5bin ()] is the path to the camlp5 binary. *)
-val camlp5bin : unit -> string
-
-(** [camlp5lib ()] is the path to the camlp5 library. *)
-val camlp5lib : unit -> string
-
 (** Coq tries to honor the XDG Base Directory Specification to access
     the user's configuration files.
 
diff --git a/lib/feedback.ml b/lib/feedback.ml
index cb8f8aad1e..9654711ebb 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -84,7 +84,7 @@ let feedback_logger ?loc lvl msg =
 let msg_info    ?loc x = feedback_logger ?loc Info x
 let msg_notice  ?loc x = feedback_logger ?loc Notice x
 let msg_warning ?loc x = feedback_logger ?loc Warning x
-let msg_error   ?loc x = feedback_logger ?loc Error x
+(* let msg_error   ?loc x = feedback_logger ?loc Error x *)
 let msg_debug   ?loc x = feedback_logger ?loc Debug x
 
 (* Helper for tools willing to understand only the messages *)
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 64fdf3724d..f407e2fd5b 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -95,11 +95,6 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit
 (** Message indicating that something went wrong, but without serious
     consequences. *)
 
-val msg_error : ?loc:Loc.t -> Pp.t -> unit
-[@@ocaml.deprecated "msg_error is an internal function and should not be \
-                     used unless you know what you are doing. Use \
-                     [CErrors.user_err] instead."]
-
 val msg_debug : ?loc:Loc.t -> Pp.t -> unit
 (** For debugging purposes *)
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 8491873e07..3aef5a7b2c 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 *)
@@ -102,14 +99,6 @@ let verbosely f x = without_option quiet f x
 let if_silent f x = if !quiet then f x
 let if_verbose f x = if not !quiet then f x
 
-let auto_intros = ref true
-let make_auto_intros flag = auto_intros := flag
-let is_auto_intros () = !auto_intros
-
-let universe_polymorphism = ref false
-let make_universe_polymorphism b = universe_polymorphism := b
-let is_universe_polymorphism () = !universe_polymorphism
-
 let polymorphic_inductive_cumulativity = ref false
 let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
 let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
@@ -124,27 +113,6 @@ let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
-(* Flags for external tools *)
-
-let browser_cmd_fmt =
- try
-  let coq_netscape_remote_var = "COQREMOTEBROWSER" in
-  Sys.getenv coq_netscape_remote_var
- with
-  Not_found -> Coq_config.browser
-
-let is_standard_doc_url url =
-  let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
-  let n = String.length Coq_config.wwwcoq in
-  let n' = String.length Coq_config.wwwrefman in
-  url = Coq_config.localwwwrefman ||
-  url = Coq_config.wwwrefman ||
-  url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
-
-(* Options for changing coqlib *)
-let coqlib_spec = ref false
-let coqlib = ref "(not initialized yet)"
-
 (* Level of inlining during a functor application *)
 
 let default_inline_level = 100
@@ -160,11 +128,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 85aaf879f3..e282d4ca8c 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
@@ -65,16 +78,9 @@ val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
 (* Miscellaneus flags for vernac *)
-val make_auto_intros : bool -> unit
-val is_auto_intros : unit -> bool
-
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
-(** Global universe polymorphism flag. *)
-val make_universe_polymorphism : bool -> unit
-val is_universe_polymorphism : unit -> bool
-
 (** Global polymorphic inductive cumulativity flag. *)
 val make_polymorphic_inductive_cumulativity : bool -> unit
 val is_polymorphic_inductive_cumulativity : unit -> bool
@@ -105,17 +111,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 (** Temporarily extends the reference to a list *)
 val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
 
-(** Options for external tools *)
-
-(** Returns string format for default browser to use from Coq or CoqIDE *)
-val browser_cmd_fmt : string
-
-val is_standard_doc_url : string -> bool
-
-(** Options for specifying where coq librairies reside *)
-val coqlib_spec : bool ref
-val coqlib : string ref
-
 (** Level of inlining during a functor application *)
 val set_inline_level : int -> unit
 val get_inline_level : unit -> int
@@ -129,13 +124,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 7a5b6f699b..b372bedc5d 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 d9e8c87b21..55f05518b0 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/genarg.mli b/lib/genarg.mli
index bb85f99e3c..52db3df088 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -13,7 +13,7 @@
 (** The route of a generic argument, from parsing to evaluation.
 In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
 
-{% \begin{%}verbatim{% }%}
+{% \begin{verbatim} %}
              parsing          in_raw                            out_raw
    char stream ---> raw_object ---> raw_object generic_argument -------+
                           encapsulation                          decaps|
@@ -36,7 +36,7 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
     |
     V
 effective use
-{% \end{%}verbatim{% }%}
+{% \end{verbatim} %}
 
 To distinguish between the uninterpreted, globalized and
 interpreted worlds, we annotate the type [generic_argument] by a
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 0891859423..206b2504db 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,11 +1,10 @@
-Coq_config
-
 Hook
 Flags
 Control
 Util
 
 Pp
+Pp_diff
 Stateid
 Loc
 Feedback
diff --git a/lib/loc.ml b/lib/loc.ml
index 6f5283aab8..1a09091bff 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -62,6 +62,11 @@ let merge_opt l1 l2 = match l1, l2 with
   | None, Some l  -> Some l
   | Some l1, Some l2 -> Some (merge l1 l2)
 
+let finer l1 l2 = match l1, l2 with
+  | None, _    -> false
+  | Some l , None -> true
+  | Some l1, Some l2 -> l1.fname = l2.fname && merge l1 l2 = l2
+
 let unloc loc = (loc.bp, loc.ep)
 
 let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp }
diff --git a/lib/loc.mli b/lib/loc.mli
index 813c45fbb3..23df1ebd9a 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -42,6 +42,10 @@ val merge : t -> t -> t
 val merge_opt : t option -> t option -> t option
 (** Merge locations, usually generating the largest possible span *)
 
+val finer : t option -> t option -> bool
+(** Answers [true] when the first location is more defined, or, when
+    both defined, included in the second one *)
+
 val shift_loc : int -> int -> t -> t
 (** [shift_loc loc n p] shifts the beginning of location by [n] and
     the end by [p]; it is assumed that the shifts do not change the
diff --git a/lib/pp.ml b/lib/pp.ml
index cd81f6e768..d68f5ac5e3 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -42,9 +42,6 @@ type doc_view =
    internal representation opaque here. *)
 type t = doc_view
 
-type std_ppcmds = t
-[@@ocaml.deprecated "alias of Pp.t"]
-
 let repr x = x
 let unrepr x = x
 
@@ -139,7 +136,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 +164,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 +308,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 f3a0a29b8a..4ce6a535c8 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -42,9 +42,6 @@ type pp_tag = string
    internal representation opaque here. *)
 type t
 
-type std_ppcmds = t
-[@@ocaml.deprecated "alias of Pp.t"]
-
 type block_type =
   | Pp_hbox   of int
   | Pp_vbox   of int
@@ -189,3 +186,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 0000000000..a485bf31c0
--- /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) = dtype 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 0000000000..03468271d2
--- /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 0e371025ea..e1c6a4c4d6 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 8edfc3d37f..5ab14f6039 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 6d2ad37872..0652623b74 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -10,19 +10,17 @@
 
 let proto_version = 0
 let prefer_sock = Sys.os_type = "Win32"
-let accept_timeout = 2.0
+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 c7a56349c6..944aa27a7f 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 a258d50527..5485c4bf19 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 dfede29e8f..a9db95318f 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,12 @@ 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
+
+(* We use argv.[0] as we don't want to resolve symlinks *)
+let get_toplevel_path ?(byte=not Dynlink.is_native) top =
+  let open Filename in
+  let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0)
+            then "" else dirname Sys.argv.(0) ^ dir_sep in
+  let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
+  let eff = if byte then ".byte" else ".opt" in
+  dir ^ top ^ eff ^ exe
diff --git a/lib/system.mli b/lib/system.mli
index 3349dfea30..f13fd30923 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 : ?byte:bool -> string -> string
diff --git a/lib/util.ml b/lib/util.ml
index 7d7d380b26..38d73d3453 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 *)