Imported Upstream version 8.5~beta1+dfsg

45 files changed, 2193 insertions, 594 deletions

diff --git a/tools/README.emacs b/tools/README.emacs
index 0d27b607..4d8e3697 100755
--- a/tools/README.emacs
+++ b/tools/README.emacs
@@ -10,14 +10,14 @@ Jean-Christophe Filliatre (jcfillia@lri.fr),
 
 CONTENTS:
 
-    coq.el         A major mode for editing Coq files in Gnu Emacs
+    gallina.el     A major mode for editing Coq files in Gnu Emacs
 
 USAGE:
 
 Add the following lines to your .emacs file:
 
 (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
 
 The Coq major mode is triggered by visiting a file with extension .v,
 or manually by M-x coq-mode. It gives you the correct syntax table for
diff --git a/tools/beautify-archive b/tools/beautify-archive
index ccfeb3db..6bfa974a 100755
--- a/tools/beautify-archive
+++ b/tools/beautify-archive
@@ -30,7 +30,7 @@ beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX`
 for i in $beaufiles; do
   j=`dirname $i`/`basename $i .v$BEAUTIFYSUFFIX`.v
   echo Upgrading $j in the beautification directory
-  mv -u -f $i $j
+  if [ $i -nt $j ]; then mv -f $i $j; fi
 done
 echo ---- Recompiling beautified files in the beautification directory -----
 make clean
@@ -44,7 +44,7 @@ vfiles=`find . -name \*.v`
 cd ..
 for i in $vfiles; do
   echo Upgrading $i in current directory
-  mv -u -f $NEWARCHIVE/$i $i
+  if [ $NEWARCHIVE/$i -nt $i ]; then mv -f $NEWARCHIVE/$i $i; fi
 done
 echo -------- Beautification completed -------------------------------------
 echo Old files are in directory '"'$OLDARCHIVE'"'
diff --git a/tools/compat5.ml b/tools/compat5.ml
index 11520c23..041ced00 100644
--- a/tools/compat5.ml
+++ b/tools/compat5.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
index e6252b11..91e3cdae 100644
--- a/tools/compat5.mlp
+++ b/tools/compat5.mlp
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
index 7f6818ee..a2336e10 100644
--- a/tools/compat5b.ml
+++ b/tools/compat5b.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
index b61b08c7..d4dfcc07 100644
--- a/tools/compat5b.mlp
+++ b/tools/compat5b.mlp
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coq-font-lock.el b/tools/coq-font-lock.el
index 05618a04..068e6400 100644
--- a/tools/coq-font-lock.el
+++ b/tools/coq-font-lock.el
@@ -110,18 +110,18 @@ syntax colouring behaviour.")
 ;;A new face for tactics
 (defface coq-solve-tactics-face
   (proof-face-specs
-   (:foreground "forestgreen" t) ; pour les fonds clairs
-   (:foreground "forestgreen"  t) ; pour les fond foncés
-   ()) ; pour le noir et blanc
+   (:foreground "forestgreen" t) ; for bright backgrounds
+   (:foreground "forestgreen"  t) ; for dark backgrounds
+   ()) ; for black and white
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
 
 ;;A new face for tactics which fail when they don't kill the current goal
 (defface coq-solve-tactics-face
   (proof-face-specs
-   (:foreground "red" t) ; pour les fonds clairs
-   (:foreground "red"  t) ; pour les fond foncés
-   ()) ; pour le noir et blanc
+   (:foreground "red" t) ; for bright backgrounds
+   (:foreground "red"  t) ; for dark backgrounds
+   ()) ; for black and white
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
 
diff --git a/tools/coq-inferior.el b/tools/coq-inferior.el
index d4f96a16..b79d97d6 100644
--- a/tools/coq-inferior.el
+++ b/tools/coq-inferior.el
@@ -46,13 +46,13 @@
 
 ;;; Installation:
 
-;; You need to have coq.el already installed (it comes with the
+;; You need to have gallina.el already installed (it comes with the
 ;; standard Coq distribution) in order to use this code.  Put this
 ;; file somewhere in you load-path and add the following lines in your
 ;; "~/.emacs":
 ;;
 ;;   (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-;;   (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+;;   (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
 ;;   (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t)
 ;;   (autoload 'run-coq-other-window "inferior-coq"
 ;;     "Run an inferior Coq process in a new window." t)
@@ -78,7 +78,7 @@
 ;; From -0.0 to 1.0 brought into existence.
 
 
-(require 'coq)
+(require 'gallina)
 (require 'comint)
 
 (setq coq-program-name "coqtop")
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 74266925..d660f420 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* créer un Makefile pour un développement Coq automatiquement *)
+(* Coq_makefile: automatically create a Makefile for a Coq development *)
 
 let output_channel = ref stdout
 let makefile_name = ref "Makefile"
@@ -32,38 +32,47 @@ let list_iter_i f =
 
 let section s =
   let l = String.length s in
-  let sep = String.make (l+5) '#'
-  and sep2 = String.make (l+5) ' ' in
-  String.set sep (l+4) '\n';
-  String.set sep2 0 '#';
-  String.set sep2 (l+3) '#';
-  String.set sep2 (l+4) '\n';
-  print sep;
-  print sep2;
+  let print_com s =
+    print "#";
+    print s;
+    print "#\n" in
+  print_com (String.make (l+2) '#');
+  print_com (String.make (l+2) ' ');
   print "# "; print s; print " #\n";
-  print sep2;
-  print sep;
+  print_com (String.make (l+2) ' ');
+  print_com (String.make (l+2) '#');
   print "\n"
 
 let usage () =
   output_string stderr "Usage summary:
 
-coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib]
-  ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath
-  logicalpath] ... [VARIABLE = value] ...  [-arg opt] ... [-opt|-byte]
-  [-no-install] [-f file] [-o file] [-h] [--help]
+coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
+  [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command]
+  ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value]
+  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
+  [-h] [--help]
 
 [file.v]: Coq file to be compiled
 [file.ml[i4]?]: Objective Caml file to be compiled
-[file.mllib]: ocamlbuild file that describes a Objective Caml library
+[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml
+  library/module
 [subdirectory] : subdirectory that should be \"made\" and has a
   Makefile itself to do so.
-[-custom command dependencies file]: add target \"file\" with command
-  \"command\" and dependencies \"dependencies\"
+[-extra result dependencies command]: add target \"result\" with command
+  \"command\" and dependencies \"dependencies\". If \"result\" is not
+  generic (do not contains a %), \"result\" is built by _make all_ and
+  deleted by _make clean_.
+[-extra-phony result dependencies command]: add a PHONY target \"result\"
+ with command \"command\" and dependencies \"dependencies\". Note that
+ _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as
+ as a dependencies of an already defined target \"foo\".
 [-I dir]: look for Objective Caml dependencies in \"dir\"
 [-R physicalpath logicalpath]: look for Coq dependencies resursively
   starting from \"physicalpath\". The logical path associated to the
   physical path is \"logicalpath\".
+[-Q physicalpath logicalpath]: look for Coq dependencies starting from
+  \"physicalpath\". The logical path associated to the physical path
+  is \"logicalpath\".
 [VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
 [-byte]: compile with byte-code version of coq
 [-opt]: compile with native-code version of coq
@@ -78,7 +87,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib]
 [--help]: equivalent to [-h]\n";
   exit 1
 
-let is_genrule r =
+let is_genrule r = (* generic rule (like bar%foo: ...) *)
     let genrule = Str.regexp("%") in
       Str.string_match genrule r 0
 
@@ -89,11 +98,11 @@ let string_prefix a b =
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
   let l2 = String.length dir2 in
-    dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/')
+    dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/')
 
 let physical_dir_of_logical_dir ldir =
   let le = String.length ldir - 1 in
-  let pdir = if ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in
+  let pdir = if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in
   for i = 0 to le - 1 do
     if pdir.[i] = '.' then pdir.[i] <- '/';
   done;
@@ -107,14 +116,15 @@ let standard opt =
   print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte");
   print "\"\n\n"
 
-let classify_files_by_root var files (inc_i,inc_r) =
-  if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then
+let classify_files_by_root var files (inc_ml,inc_i,inc_r) =
+  if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r)
+    && not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_i) then
     begin
       let absdir_of_files = List.rev_map
-	(fun x -> Minilib.canonical_path_name (Filename.dirname x))
+	(fun x -> CUnix.canonical_path_name (Filename.dirname x))
 	files in
 	(* files in scope of a -I option (assuming they are no overlapping) *)
-      let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in
+      let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml in
 	if has_inc_i then
 	  begin
 	    printf "%sINC=" var;
@@ -123,128 +133,188 @@ let classify_files_by_root var files (inc_i,inc_r) =
 			 then printf
 			   "$(filter $(wildcard %s/*),$(%s)) "
 			   pdir var
-		      ) inc_i;
+		      ) inc_ml;
 	    printf "\n";
 	  end;
       (* Files in the scope of a -R option (assuming they are disjoint) *)
-	list_iter_i (fun i (pdir,ldir,abspdir) ->
+	list_iter_i (fun i (pdir,_,abspdir) ->
 		       if List.exists (is_prefix abspdir) absdir_of_files then
 			 printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
 			   var i pdir pdir var)
-	  inc_r;
+	  (inc_i@inc_r);
     end
 
-let install_include_by_root files_var files (inc_i,inc_r) =
-  try
+let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
+  let var_x_absdirs_l = List.rev_map
+    (fun (v,l) -> (v,List.rev_map (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l))
+    var_x_files_l in
+  let var_filter f g = List.fold_left (fun acc (var,dirs) ->
+    if f dirs
+    then (g var)::acc else acc) [] var_x_absdirs_l in
     (* All files caught by a -R . option (assuming it is the only one) *)
-    let ldir = match inc_r with
-      |[(".",t,_)] -> t
-      |l -> let out = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in
-	 let () = prerr_string "Warning: install rule assumes that -R . _ is the only -R option" in
-	   out in
-    let pdir = physical_dir_of_logical_dir ldir in
-      printf "\tfor i in $(%s); do \\\n" files_var;
-      printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir;
-      printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir;
-      printf "\tdone\n"
-  with Not_found ->
-    let absdir_of_files = List.rev_map
-      (fun x -> Minilib.canonical_path_name (Filename.dirname x))
-      files in
-    let has_inc_i_files =
-      List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in
-    let install_inc_i d =
-      printf "\tinstall -d $(DSTROOT)$(COQLIBINSTALL)/%s; \\\n" d;
-      printf "\tfor i in $(%sINC); do \\\n" files_var;
-      printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" d;
+  match inc_i@inc_r with
+  |[(".",t,_)] -> (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l])
+  |l ->
+    try
+      let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
+      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option" in
+      (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
+    with Not_found ->
+      (
+      (* vars for -Q options *)
+	Some (var_filter (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) (fun x -> x)),
+      (* (physical dir, physical dir of logical path,vars) for -R options
+	 (assuming physical dirs are disjoint) *)
+      if l = [] then
+	[".","$(INSTALLDEFAULTROOT)",[]]
+      else
+	Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) ->
+	  let vars_r = var_filter (List.exists (is_prefix abspdir)) (fun x -> x^string_of_int i) in
+	  let pdir' = physical_dir_of_logical_dir ldir in
+	  (pdir,pdir',vars_r)::out) 1 [] l
+      )
+
+let install_include_by_root perms =
+  let install_dir for_i (pdir,pdir',vars) =
+    let b = vars <> [] in
+    if b then begin
+      printf "\tcd \"%s\" && for i in " pdir;
+      print_list " " (List.rev_map (Format.sprintf "$(%s)") vars);
+      print "; do \\\n";
+      printf "\t install -d \"`dirname \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i`\"; \\\n" pdir';
+      printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i; \\\n" perms pdir';
+      printf "\tdone\n";
+    end;
+    for_i b pdir' in
+  let install_i = function
+    |[] -> fun _ _ -> ()
+    |l -> fun b d ->
+      if not b then printf "\tinstall -d \"$(DSTROOT)\"$(COQLIBINSTALL)/%s; \\\n" d;
+      print "\tfor i in ";
+      print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l);
+      print "; do \\\n";
+      printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" perms d;
       printf "\tdone\n"
-    in
-      if inc_r = [] then
-	if has_inc_i_files then
-	  begin
-	    (* Files in the scope of a -I option *)
-	    install_inc_i "$(INSTALLDEFAULTROOT)";
-	  end else ()
+  in function
+  |None,l -> List.iter (install_dir (fun _ _ -> ())) l
+  |Some v_i,l -> List.iter (install_dir (install_i v_i)) l
+
+let uninstall_by_root =
+  let uninstall_dir for_i (pdir,pdir',vars) =
+    printf "\tprintf 'cd \"$${DSTROOT}\"$(COQLIBINSTALL)/%s" pdir';
+    if vars <> [] then begin
+      print " && rm -f ";
+      print_list " " (List.rev_map (Format.sprintf "$(%s)") vars);
+    end;
+    for_i ();
+    print " && find . -type d -and -empty -delete\\n";
+    print "cd \"$${DSTROOT}\"$(COQLIBINSTALL) && ";
+    printf "find \"%s\" -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" pdir'
+in
+  let uninstall_i = function
+    |[] -> ()
+    |l ->
+      print " && \\\\\\nfor i in ";
+      print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l);
+      print "; do rm -f \"`basename \"$$i\"`\"; done"
+  in function
+  |None,l -> List.iter (uninstall_dir (fun _ -> ())) l
+  |Some v_i,l -> List.iter (uninstall_dir (fun () -> uninstall_i v_i)) l
+
+let where_put_doc = function
+    |_,[],[] -> "$(INSTALLDEFAULTROOT)";
+    |_,((_,lp,_)::q as inc_i),[] ->
+      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
+      if (pr <> "") &&
+	((List.exists (fun(_,b,_) -> b = pr) inc_i)
+	 || pr.[String.length pr - 1] = '.')
+      then
+	physical_dir_of_logical_dir pr
       else
-	(* Files in the scope of a -R option (assuming they are disjoint) *)
-	list_iter_i (fun i (pdir,ldir,abspdir) ->
-		       let has_inc_r_files = List.exists (is_prefix abspdir) absdir_of_files in
-		       let pdir' = physical_dir_of_logical_dir ldir in
-			 if has_inc_r_files then
-			   begin
-			     printf "\tcd %s; for i in $(%s%d); do \\\n" pdir files_var i;
-			     printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir';
-			     printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir';
-			     printf "\tdone\n";
-			   end;
-			 if has_inc_i_files then install_inc_i pdir'
-		    ) inc_r
-
-let install_doc some_vfiles some_mlifiles (_,inc_r) =
-  let install_one_kind kind dir =
-    printf "\tinstall -d $(DSTROOT)$(COQDOCINSTALL)/%s/%s\n" dir kind;
-    printf "\tfor i in %s/*; do \\\n" kind;
-    printf "\t install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/%s/$$i;\\\n" dir;
-    print "\tdone\n" in
-    print "install-doc:\n";
-    let () = match inc_r with
-      |[] ->
-	 if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)";
-	  if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)";
-      |(_,lp,_)::q ->
-	 let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
-	   if (pr <> "") &&
-	     ((List.exists (fun(_,b,_) -> b = pr) inc_r) || pr.[String.length pr - 1] = '.')
-	   then begin
-	     let rt = physical_dir_of_logical_dir pr in
-	       if some_vfiles then install_one_kind "html" rt;
-	       if some_mlifiles then install_one_kind "mlihtml" rt;
-	   end else begin
-	     prerr_string "Warning: -R options don't have a correct common prefix,
- install-doc will put anything in $INSTALLDEFAULTROOT\n";
-	   if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)";
-	   if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)";
-	   end in
-      print "\n"
+	let () = prerr_string "Warning: -Q options don't have a correct common prefix,
+ install-doc will put anything in $INSTALLDEFAULTROOT\n" in
+	"$(INSTALLDEFAULTROOT)"
+    |_,inc_i,((_,lp,_)::q as inc_r) ->
+      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
+      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) pr inc_i in
+      if (pr <> "") &&
+	((List.exists (fun(_,b,_) -> b = pr) inc_r)
+	 || (List.exists (fun(_,b,_) -> b = pr) inc_i)
+	 || pr.[String.length pr - 1] = '.')
+      then
+	physical_dir_of_logical_dir pr
+      else
+	let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix,
+ install-doc will put anything in $INSTALLDEFAULTROOT\n" in
+	"$(INSTALLDEFAULTROOT)"
 
 let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function
   |Project_file.NoInstall -> ()
   |is_install ->
+    let not_empty = function |[] -> false |_::_ -> true in
+    let cmofiles = List.rev_append mlpackfiles (List.rev_append mlfiles ml4files) in
+    let cmifiles = List.rev_append mlifiles cmofiles in
+    let cmxsfiles = List.rev_append cmofiles mllibfiles in
+    let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in
+    let where_what_oth = vars_to_put_by_root
+      [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)]
+      inc in
+    let doc_dir = where_put_doc inc in
     let () = if is_install = Project_file.UnspecInstall then
 	print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" in
-  let not_empty = function |[] -> false |_::_ -> true in
-  let cmofiles = mlpackfiles@mlfiles@ml4files in
-  let cmifiles = mlifiles@cmofiles in
-  let cmxsfiles = cmofiles@mllibfiles in
     if (not_empty cmxsfiles) then begin
       print "install-natdynlink:\n";
-      install_include_by_root "CMXSFILES" cmxsfiles inc;
+      install_include_by_root "0755" where_what_cmxs;
+      print "\n";
+    end;
+    if (not_empty cmxsfiles) then begin
+      print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
+      printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
+      printf "\t install -m 0755 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
       print "\n";
     end;
     print "install:";
     if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
     print "\n";
-    if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc;
-    if (not_empty cmofiles) then
-      install_include_by_root "CMOFILES" cmofiles inc;
-    if (not_empty cmifiles) then
-      install_include_by_root "CMIFILES" cmifiles inc;
-    if (not_empty mllibfiles) then
-      install_include_by_root "CMAFILES" mllibfiles inc;
+    install_include_by_root "0644" where_what_oth;
     List.iter
       (fun x ->
-	 printf "\t(cd %s; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x)
+	printf "\t+cd %s && $(MAKE) DSTROOT=\"$(DSTROOT)\" INSTALLDEFAULTROOT=\"$(INSTALLDEFAULTROOT)/%s\" install\n" x x)
       sds;
     print "\n";
-    install_doc (not_empty vfiles) (not_empty mlifiles) inc
+    let install_one_kind kind dir =
+      printf "\tinstall -d \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/%s\n" dir kind;
+      printf "\tfor i in %s/*; do \\\n" kind;
+      printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/$$i;\\\n" dir;
+      print "\tdone\n" in
+    print "install-doc:\n";
+    if not_empty vfiles then install_one_kind "html" doc_dir;
+    if not_empty mlifiles then install_one_kind "mlihtml" doc_dir;
+    print "\n";
+    let uninstall_one_kind kind dir =
+      printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir;
+      printf "\tprintf '&& rm -f $(shell find \"%s\" -maxdepth 1 -and -type f -print)\\n' >> \"$@\"\n" kind;
+      print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && ";
+      printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind
+    in
+    print "uninstall_me.sh:\n";
+    print "\techo '#!/bin/sh' > $@ \n";
+    if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs;
+    uninstall_by_root where_what_oth;
+    if not_empty vfiles then uninstall_one_kind "html" doc_dir;
+    if not_empty mlifiles then uninstall_one_kind "mlihtml" doc_dir;
+    print "\tchmod +x $@\n";
+    print "\n";
+    print "uninstall: uninstall_me.sh\n";
+    print "\tsh $<\n\n"
 
 let make_makefile sds =
   if !make_name <> "" then begin
     printf "%s: %s\n" !makefile_name !make_name;
     print "\tmv -f $@ $@.bak\n";
-    print "\t$(COQBIN)coq_makefile -f $< -o $@\n\n";
+    print "\t\"$(COQBIN)coq_makefile\" -f $< -o $@\n\n";
     List.iter
-      (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n")
+      (fun x -> print "\t+cd "; print x; print " && $(MAKE) Makefile\n")
       sds;
     print "\n";
   end
@@ -257,71 +327,78 @@ let clean sds sps =
     print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n";
   end;
   if !some_vfile then
-    print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n";
+    begin
+      print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n";
+      print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"
+    end;
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
-  print "\t- rm -rf html mlihtml\n";
+  print "\t- rm -rf html mlihtml uninstall_me.sh\n";
   List.iter
-    (fun (file,_,_) ->
-       if not (is_genrule file) then
+    (fun (file,_,is_phony,_) ->
+       if not (is_phony || is_genrule file) then
 	 (print "\t- rm -rf "; print file; print "\n"))
     sps;
   List.iter
-    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n")
+    (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n")
     sds;
   print "\n";
   print "archclean:\n";
   print "\trm -f *.cmx *.o\n";
   List.iter
-    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
+    (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n")
     sds;
   print "\n";
-  print "printenv:\n\t@$(COQBIN)coqtop -config\n";
-  print "\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n\t@echo PP =\t$(PP)\n\t@echo COQFLAGS =\t$(COQFLAGS)\n";
-  print "\t@echo COQLIBINSTALL =\t$(COQLIBINSTALL)\n\t@echo COQDOCINSTALL =\t$(COQDOCINSTALL)\n\n"
+  print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n";
+  print "\t@echo 'CAMLC =\t$(CAMLC)'\n\t@echo 'CAMLOPTC =\t$(CAMLOPTC)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
+  print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n"
 
 let header_includes () = ()
 
 let implicit () =
     section "Implicit rules.";
   let mli_rules () =
-    print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "%.mli.d: %.mli\n";
+    print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+    print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n";
     print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let ml4_rules () =
-    print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "%.ml4.d: %.ml4\n";
-    print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
+    print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n";
+    print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
+    print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
+    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let ml_rules () =
-    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "%.ml.d: %.ml\n";
+    print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+    print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n";
+    print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+    print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n";
     print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
-  let cmxs_rules () =
-    print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n";
-    print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in
+  let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *)
+    print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx
+\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n";
+    print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" in
   let mllib_rules () =
-    print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
-    print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
-    print "%.mllib.d: %.mllib\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
+    print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
+    print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n";
+    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let mlpack_rules () =
-    print "%.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
-    print "%.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
-    print "%.mlpack.d: %.mlpack\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+    print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
+    print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
+    print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n";
+    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
 in
   let v_rules () =
-    print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
-    print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
-    print "%.g: %.v\n\t$(GALLINA) $<\n\n";
-    print "%.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
-    print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
-    print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
-    print "%.g.html: %.v %.glob\n\t$(COQDOC)$(COQDOCFLAGS)  -html -g $< -o $@\n\n";
-    print "%.v.d: %.v\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
-    print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
+    print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
+    print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
+    print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n";
+    print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n";
+    print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
+    print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
+    print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
+    print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@\n\n";
+    print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n";
+    print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+    print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
   in
     if !some_mlifile then mli_rules ();
     if !some_ml4file then ml4_rules ();
@@ -350,100 +427,121 @@ let variables is_install opt (args,defs) =
     end;
     (* Coq executables and relative variables *)
     if !some_vfile || !some_mlpackfile || !some_mllibfile then
-      print "COQDEP?=$(COQBIN)coqdep -c\n";
+      print "COQDEP?=\"$(COQBIN)coqdep\" -c\n";
     if !some_vfile then begin
     print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
     print "COQCHKFLAGS?=-silent -o\n";
     print "COQDOCFLAGS?=-interpolate -utf8\n";
-    print "COQC?=$(COQBIN)coqc\n";
-    print "GALLINA?=$(COQBIN)gallina\n";
-    print "COQDOC?=$(COQBIN)coqdoc\n";
-    print "COQCHK?=$(COQBIN)coqchk\n\n";
+    print "COQC?=$(TIMER) \"$(COQBIN)coqc\"\n";
+    print "GALLINA?=\"$(COQBIN)gallina\"\n";
+    print "COQDOC?=\"$(COQBIN)coqdoc\"\n";
+    print "COQCHK?=\"$(COQBIN)coqchk\"\n";
+    print "COQMKTOP?=\"$(COQBIN)coqmktop\"\n\n";
     end;
     (* Caml executables and relative variables *)
     if !some_ml4file || !some_mlfile || !some_mlifile then begin
-    print "COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \\
-  -I $(COQLIB)library -I $(COQLIB)parsing \\
-  -I $(COQLIB)pretyping -I $(COQLIB)interp \\
-  -I $(COQLIB)proofs -I $(COQLIB)tactics \\
-  -I $(COQLIB)toplevel";
+    print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\
+  -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)pretyping\" \\
+  -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\
+  -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\
+  -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\
+  -I \"$(COQLIB)config\"";
     List.iter (fun c -> print " \\
-  -I $(COQLIB)plugins/"; print c) Coq_config.plugins_dirs; print "\n";
+  -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
-    print "CAMLC?=$(OCAMLC) -c -rectypes\n";
-    print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n";
-    print "CAMLLINK?=$(OCAMLC) -rectypes\n";
-    print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n";
+    print "CAMLC?=$(OCAMLC) -c -rectypes -thread\n";
+    print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread\n";
+    print "CAMLLINK?=$(OCAMLC) -rectypes -thread\n";
+    print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread\n";
     print "GRAMMARS?=grammar.cma\n";
-    print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
-    print "CAMLP4OPTIONS?=-loc loc\n";
-    print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n";
+    print "ifeq ($(CAMLP4),camlp5)
+CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
+else
+CAMLP4EXTEND=
+endif\n";
+    print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\
+  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
     end;
     match is_install with
       | Project_file.NoInstall -> ()
       | Project_file.UnspecInstall ->
         section "Install Paths.";
 	print "ifdef USERINSTALL\n";
-        print "XDG_DATA_HOME?=$(HOME)/.local/share\n";
+        print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
         print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
         print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n";
 	print "else\n";
-        print "COQLIBINSTALL=${COQLIB}user-contrib\n";
-        print "COQDOCINSTALL=${DOCDIR}user-contrib\n";
+        print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
+        print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
+        print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
 	print "endif\n\n"
       | Project_file.TraditionalInstall ->
           section "Install Paths.";
-          print "COQLIBINSTALL=${COQLIB}user-contrib\n";
-          print "COQDOCINSTALL=${DOCDIR}user-contrib\n";
+          print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
+          print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
+          print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
           print "\n"
       | Project_file.UserInstall ->
           section "Install Paths.";
-          print "XDG_DATA_HOME?=$(HOME)/.local/share\n";
+          print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
           print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
           print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n";
+          print "COQTOPINSTALL=$(XDG_DATA_HOME)/coq/toploop\n";
           print "\n"
 
 let parameters () =
   print ".DEFAULT_GOAL := all\n\n# \n";
   print "# This Makefile may take arguments passed as environment variables:\n";
   print "# COQBIN to specify the directory where Coq binaries resides;\n";
+  print "# TIMECMD set a command to log .v compilation time;\n";
+  print "# TIMED if non empty, use the default time command as TIMECMD;\n";
   print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n";
   print "# DSTROOT to specify a prefix to install path.\n\n";
   print "# Here is a hack to make $(eval $(shell works:\n";
   print "define donewline\n\n\nendef\n";
   print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n";
-  print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"
-
-let include_dirs (inc_i,inc_r) =
-  let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in
-  let parse_rec_includes l =
-    List.map (fun (p,l,_) ->
-      let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l')
-      l in
-  let inc_i' = List.filter (fun (_,i) -> not (List.exists (fun (_,_,i') -> is_prefix i' i) inc_r)) inc_i in
+  print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
+  print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
+  print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
+  print "vo_to_obj = $(addsuffix .o,\\\n";
+  print "  $(filter-out Warning: Error:,\\\n";
+  print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
+
+let include_dirs (inc_ml,inc_i,inc_r) =
+  let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
+  let parse_includes l = List.map (fun (x,l,_) ->
+				   let l' = if l = "" then "\"\"" else l in
+				   "-Q \"" ^ x ^ "\" " ^ l' ^"") l in
+  let parse_rec_includes l = List.map (fun (p,l,_) ->
+				       let l' = if l = "" then "\"\"" else l in
+				       "-R \"" ^ p ^ "\" " ^ l' ^"") l in
+  let str_ml = parse_ml_includes inc_ml in
   let str_i = parse_includes inc_i in
-  let str_i' = parse_includes inc_i' in
   let str_r = parse_rec_includes inc_r in
     section "Libraries definitions.";
     if !some_ml4file || !some_mlfile || !some_mlifile then begin
-      print "OCAMLLIBS?="; print_list "\\\n  " str_i; print "\n";
+      print "OCAMLLIBS?="; print_list "\\\n  " str_ml; print "\n";
     end;
     if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
-      print "COQLIBS?="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
-      print "COQDOCLIBS?=";   print_list "\\\n  " str_r; print "\n\n";
+      print "COQLIBS?="; print_list "\\\n  " str_i;
+      List.iter (fun x -> print "\\\n  "; print x) str_r;
+      List.iter (fun x -> print "\\\n  "; print x) str_ml; print "\n";
+      print "COQDOCLIBS?="; print_list "\\\n  " str_i;
+      List.iter (fun x -> print "\\\n  "; print x) str_r; print "\n\n";
     end
 
 let custom sps =
-  let pr_path (file,dependencies,com) =
+  let pr_path (file,dependencies,is_phony,com) =
     print file; print ": "; print dependencies; print "\n";
-    if com <> "" then (print "\t"; print com); print "\n\n"
+    if com <> "" then (print "\t"; print com; print "\n");
+    print "\n"
   in
     if sps <> [] then section "Custom targets.";
     List.iter pr_path sps
 
 let subdirs sds =
   let pr_subdir s =
-    print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n"
+    print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n"
   in
     if sds <> [] then section "Subdirectories.";
     List.iter pr_subdir sds
@@ -470,13 +568,17 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
   begin match vfiles with
     |[] -> ()
     |l ->
-      print "VOFILES:=$(VFILES:.v=.vo)\n";
+      print "VO=vo\n";
+      print "VOFILES:=$(VFILES:.v=.$(VO))\n";
       classify_files_by_root "VOFILES" l inc;
       print "GLOBFILES:=$(VFILES:.v=.glob)\n";
-      print "VIFILES:=$(VFILES:.v=.vi)\n";
       print "GFILES:=$(VFILES:.v=.g)\n";
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
-      print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"
+      print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
+      print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n";
+      print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n";
+      classify_files_by_root "NATIVEFILES" l inc
   end;
   decl_var "ML4FILES" ml4files;
   decl_var "MLFILES" mlfiles;
@@ -566,7 +668,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     end;
   if !some_vfile then
     begin
-      print "spec: $(VIFILES)\n\n";
+      print "quick: $(VOFILES:.vo=.vio)\n\n";
+      print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n";
+      print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n";
       print "gallina: $(GFILES)\n\n";
       print "html: $(GLOBFILES) $(VFILES)\n";
       print "\t- mkdir -p html\n";
@@ -591,13 +695,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     end
 
 let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
-  let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in
-  let other_targets = List.map (function x,_,_ -> x) special_targets @ sds in
+  let other_targets = CList.map_filter
+    (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None)
+    sps @ sds in
   main_targets vfiles mlfiles other_targets inc;
     print ".PHONY: ";
     print_list " "
-      ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install"
-	:: "userinstall" :: "depend" :: "html" :: "validate" :: sds);
+      ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install" ::
+	  "uninstall_me.sh" :: "uninstall" :: "userinstall" :: "depend" ::
+	  "html" :: "validate" ::
+	    (sds@(CList.map_filter
+		    (fun (n,_,is_phony,_) ->
+		     if is_phony then Some n else None) sps)));
     print "\n\n";
     custom sps;
     subdirs sds;
@@ -628,38 +737,38 @@ let command_line args =
   print_list args;
   print "\n#\n\n"
 
-let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((i_inc,r_inc) as l) =
+let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l) =
   let here = Sys.getcwd () in
   let not_tops =List.for_all (fun s -> s <> Filename.basename s) in
-  if List.exists (fun (_,x) -> x = here) i_inc
-    or List.exists (fun (_,_,x) -> is_prefix x here) r_inc
-    or (not_tops v && not_tops mli && not_tops ml4 && not_tops ml
+  if List.exists (fun (_,_,x) -> x = here) i_inc
+    || List.exists (fun (_,_,x) -> is_prefix x here) r_inc
+    || (not_tops v && not_tops mli && not_tops ml4 && not_tops ml
 	&& not_tops mllib && not_tops mlpack) then
     l
   else
-    ((".",here)::i_inc,r_inc)
+    ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc)
 
 let warn_install_at_root_directory
-    (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_i,inc_r) =
-  let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in
-  let inc_top = List.map (fun (p,_,_) -> p) inc_r_top in
+    (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) =
+  let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r@inc_i in
+  let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in
   let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in
-  if inc_r = [] || List.exists (fun f -> List.mem (Filename.dirname f) inc_top) files
+  if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files
   then
-    Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n"
-      (if inc_r_top = [] then "" else "with non trivial logical root ")
+    Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n"
+      (if inc_top = [] then "" else "with non trivial logical root ")
 
-let check_overlapping_include (_,inc_r) =
+let check_overlapping_include (_,inc_i,inc_r) =
   let pwd = Sys.getcwd () in
-  let rec aux = function
+  let aux = function
     | [] -> ()
     | (pdir,_,abspdir)::l ->
 	if not (is_prefix pwd abspdir) then
 	  Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir;
 	List.iter (fun (pdir',_,abspdir') ->
-	  if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then
+	  if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
 	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
-  in aux inc_r
+  in aux (inc_i@inc_r)
 
 let do_makefile args =
   let has_file var = function
@@ -686,7 +795,7 @@ let do_makefile args =
     else if (Filename.check_suffix f ".mllib") then some_mllibfile := true
     else if (Filename.check_suffix f ".mlpack") then some_mlpackfile := true
   in
-  List.iter (fun (_,dependencies,_) ->
+  List.iter (fun (_,dependencies,_,_) ->
     List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
 
   let inc = ensure_root_dir targets inc in
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index ca21f706..383a68df 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -79,7 +79,7 @@ let expos   = Str.regexp "^"
 
 let tex_escaped s =
   let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
-  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in
+  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>']") in
   let adapt_delim = function
     | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
     | "\\" -> "{\\char'134}"
@@ -88,6 +88,7 @@ let tex_escaped s =
     | " " -> "~"
     | "<" -> "{<}"
     | ">" -> "{>}"
+    | "'" -> "{\\textquotesingle}"
     | _ -> assert false
   in
   let adapt = function
@@ -116,7 +117,7 @@ let insert texfile coq_output result =
   let next_block k =
     if !last_read = "" then last_read := input_line c_coq;
     (* skip k prompts *)
-    for i = 1 to k do
+    for _i = 1 to k do
       last_read := remove_prompt !last_read;
     done;
     (* read and return the following lines until a prompt is found *)
@@ -170,9 +171,10 @@ let insert texfile coq_output result =
     if Str.string_match end_coq_example s 0 then begin
       just_after ()
     end else begin
-      if !verbose then Printf.printf "Coq < %s\n" s;
-      if (not first_block) & k=0 then output_string c_out "\\medskip\n";
-      if show_questions then encapsule false c_out ("Coq < " ^ s);
+      let prompt = if k = 0 then "Coq < " else "      " in
+      if !verbose then Printf.printf "%s%s\n" prompt s;
+      if (not first_block) && k=0 then output_string c_out "\\medskip\n";
+      if show_questions then encapsule false c_out (prompt ^ s);
       if has_match dot_end_line s then begin
 	let bl = next_block (succ k) in
 	if !verbose then List.iter print_endline bl;
@@ -209,7 +211,7 @@ let insert texfile coq_output result =
 
 (* Process of one TeX file *)
 
-let rm f = try Sys.remove f with _ -> ()
+let rm f = try Sys.remove f with any -> ()
 
 let one_file texfile =
   let inputv = Filename.temp_file "coq_tex" ".v" in
@@ -233,9 +235,9 @@ let one_file texfile =
     insert texfile coq_output result;
     (* 4. clean up *)
     rm inputv; rm coq_output
-  with e -> begin
+  with reraise -> begin
     rm inputv; rm coq_output;
-    raise e
+    raise reraise
   end
 
 (* Parsing of the command line, check of the Coq command and process
diff --git a/tools/coqc.ml b/tools/coqc.ml
new file mode 100644
index 00000000..f636ffd8
--- /dev/null
+++ b/tools/coqc.ml
@@ -0,0 +1,184 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Coq compiler : coqc *)
+
+(** For improving portability, coqc is now an OCaml program instead
+    of a shell script. We use as much as possible the Sys and Filename
+    module for better portability, but the Unix module is still used
+    here and there (with explicitly qualified function names Unix.foo).
+
+    We process here the commmand line to extract names of files to compile,
+    then we compile them one by one while passing by the rest of the command
+    line to a process running "coqtop -batch -compile <file>".
+*)
+
+(* Environment *)
+
+let environment = Unix.environment ()
+
+let binary = ref "coqtop"
+let image = ref ""
+
+let verbose = ref false
+
+let rec make_compilation_args = function
+  | [] -> []
+  | file :: fl ->
+      let file_noext =
+        if Filename.check_suffix file ".v" then
+          Filename.chop_suffix file ".v"
+        else file
+      in
+      (if !verbose then "-compile-verbose" else "-compile")
+      :: file_noext :: (make_compilation_args fl)
+
+(* compilation of files [files] with command [command] and args [args] *)
+
+let compile command args files =
+  let args' = command :: args @ (make_compilation_args files) in
+  match Sys.os_type with
+  | "Win32" ->
+     let pid =
+        Unix.create_process_env command (Array.of_list args') environment
+        Unix.stdin Unix.stdout Unix.stderr
+     in
+     let status = snd (Unix.waitpid [] pid) in
+     let errcode =
+       match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c
+     in
+     exit errcode
+  | _ ->
+     Unix.execvpe command (Array.of_list args') environment
+
+let usage () =
+  Usage.print_usage_coqc () ;
+  flush stderr ;
+  exit 1
+
+(* parsing of the command line *)
+let extra_arg_needed = ref true
+
+let parse_args () =
+  let rec parse (cfiles,args) = function
+    | [] ->
+	List.rev cfiles, List.rev args
+    | ("-verbose" | "--verbose") :: rem ->
+	verbose := true ; parse (cfiles,args) rem
+    | "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
+    | "-image" :: [] ->	usage ()
+    | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
+    | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem
+
+(* Obsolete options *)
+
+    | "-libdir" :: _ :: rem ->
+        print_string "Warning: option -libdir deprecated and ignored\n";
+        flush stdout;
+        parse (cfiles,args) rem
+    | ("-db"|"-debugger") :: rem ->
+        print_string "Warning: option -db/-debugger deprecated and ignored\n";
+        flush stdout;
+        parse (cfiles,args) rem
+
+(* Informative options *)
+
+    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
+
+    | ("-v"|"--version") :: _ -> Usage.version 0
+
+    | ("-where") :: _ ->
+        Envars.set_coqlib (fun x -> x);
+        print_endline (Envars.coqlib ());
+        exit 0
+
+    | ("-config" | "--config") :: _ ->
+        Envars.set_coqlib (fun x -> x);
+        Usage.print_config ();
+        exit 0
+
+(* Options for coqtop : a) options with 0 argument *)
+
+    | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"
+      |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
+      |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
+      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
+      |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
+      |"-impredicative-set"|"-vm"|"-no-native-compiler"
+      |"-verbose-compat-notations"|"-no-compat-notations"
+      |"-indices-matter"|"-quick"|"-color"
+      |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
+      as o) :: rem ->
+	parse (cfiles,o::args) rem
+
+(* Options for coqtop : b) options with 1 argument *)
+
+    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
+      |"-load-vernac-source"|"-l"|"-load-vernac-object"
+      |"-load-ml-source"|"-require"|"-load-ml-object"
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
+      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
+      as o) :: rem ->
+	begin
+	  match rem with
+	    | s :: rem' -> parse (cfiles,s::o::args) rem'
+	    | []        -> usage ()
+	end
+
+(* Options for coqtop : c) options with 1 argument and possibly more *)
+
+    | ("-I"|"-include" as o) :: rem ->
+	begin
+	  match rem with
+	  | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
+	  | s :: "-as" :: [] -> usage ()
+	  | s :: rem' -> parse (cfiles,s::o::args) rem'
+	  | []        -> usage ()
+	end
+    | "-R" :: s :: "-as" :: t :: rem ->	parse (cfiles,t::"-as"::s::"-R"::args) rem
+    | "-R" :: s :: "-as" :: [] -> usage ()
+    | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
+    | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem
+    | ("-schedule-vio-checking"
+      |"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem ->
+        let nodash, rem =
+          CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
+        extra_arg_needed := false;
+        parse (cfiles, List.rev nodash @ s :: o :: args) rem
+
+    | f :: rem ->
+	if Sys.file_exists f then
+	  parse (f::cfiles,args) rem
+	else
+	  let fv = f ^ ".v" in
+	  if Sys.file_exists fv then
+	    parse (fv::cfiles,args) rem
+	  else begin
+	    prerr_endline ("coqc: "^f^": no such file or directory") ;
+	    exit 1
+	  end
+  in
+  parse ([],[]) (List.tl (Array.to_list Sys.argv))
+
+(* main: we parse the command line, define the command to compile files
+ * and then call the compilation on each file *)
+
+let main () =
+  let cfiles, args = parse_args () in
+    if cfiles = [] && !extra_arg_needed then begin
+      prerr_endline "coqc: too few arguments" ;
+      usage ()
+    end;
+    let coqtopname =
+      if !image <> "" then !image
+      else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension)
+    in
+      (*  List.iter (compile coqtopname args) cfiles*)
+      Unix.handle_unix_error (compile coqtopname args) cfiles
+
+let _ = Printexc.print main ()
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 21b4e576..2e0cce6e 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,8 +19,9 @@ open Coqdep_common
 let option_D = ref false
 let option_w = ref false
 let option_sort = ref false
+let option_dump = ref None
 
-let rec warning_mult suf iter =
+let warning_mult suf iter =
   let tab = Hashtbl.create 151 in
   let check f d =
     begin try
@@ -35,11 +36,11 @@ let rec warning_mult suf iter =
   in
   iter check
 
-let add_coqlib_known phys_dir log_dir f =
+let add_coqlib_known recur phys_dir log_dir f =
   match get_extension f [".vo"] with
     | (basename,".vo") ->
         let name = log_dir@[basename] in
-	let paths = suffixes name in
+	let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
@@ -120,7 +121,7 @@ let traite_Declare f =
 	let s' = basename_noext s in
 	(match search_ml_known s with
 	   | Some mldir when not (List.mem s' !decl_list) ->
-	       let fullname = file_name (String.uncapitalize s') mldir in
+	       let fullname = file_name s' mldir in
 	       let depl = mL_dep_list s (fullname ^ ".ml") in
 	       treat depl;
 	       decl_list := s :: !decl_list
@@ -156,35 +157,319 @@ let declare_dependencies () =
        flush stdout)
     (List.rev !vAccu)
 
+(** DAGs guaranteed to be transitive reductions *)
+module DAG (Node : Set.OrderedType) :
+sig
+  type node = Node.t
+  type t
+  val empty : t
+  val add_transitive_edge : node -> node -> t -> t
+  val iter : (node -> node -> unit) -> t -> unit
+end =
+struct
+  type node = Node.t
+  module NSet = Set.Make(Node)
+  module NMap = Map.Make(Node)
+
+  (** Associate to a node the set of its neighbours *)
+  type _t = NSet.t NMap.t
+
+  (** Optimisation: construct the reverse graph at the same time *)
+  type t = { dir : _t; rev : _t; }
+
+
+  let node_equal x y = Node.compare x y = 0
+
+  let add_edge x y graph =
+    let set = try NMap.find x graph with Not_found -> NSet.empty in
+    NMap.add x (NSet.add y set) graph
+
+  let remove_edge x y graph =
+    let set = try NMap.find x graph with Not_found -> NSet.empty in
+    let set = NSet.remove y set in
+    if NSet.is_empty set then NMap.remove x graph
+    else NMap.add x set graph
+
+  let has_edge x y graph =
+    let set = try NMap.find x graph with Not_found -> NSet.empty in
+    NSet.mem y set
+
+  let connected x y graph =
+    let rec aux rem seen =
+      if NSet.is_empty rem then false
+      else
+        let x = NSet.choose rem in
+        if node_equal x y then true
+        else
+          let rem = NSet.remove x rem in
+          if NSet.mem x seen then
+            aux rem seen
+          else
+            let seen = NSet.add x seen in
+            let next = try NMap.find x graph with Not_found -> NSet.empty in
+            let rem = NSet.union next rem in
+            aux rem seen
+    in
+    aux (NSet.singleton x) NSet.empty
+
+  (** Check whether there is a path from a to b going through the edge
+      x -> y. *)
+  let connected_through a b x y graph =
+    let rec aux rem seen =
+      if NMap.is_empty rem then false
+      else
+        let (n, through) = NMap.choose rem in
+        if node_equal n b && through then true
+        else
+          let rem = NMap.remove n rem in
+          let is_seen = try Some (NMap.find n seen) with Not_found -> None in
+          match is_seen with
+          | None ->
+            let seen = NMap.add n through seen in
+            let next = try NMap.find n graph with Not_found -> NSet.empty in
+            let is_x = node_equal n x in
+            let push m accu =
+              let through = through || (is_x && node_equal m y) in
+              NMap.add m through accu
+            in
+            let rem = NSet.fold push next rem in
+            aux rem seen
+          | Some false ->
+            (** The path we took encountered x -> y but not the one in seen *)
+            if through then aux (NMap.add n true rem) (NMap.add n true seen)
+            else aux rem seen
+          | Some true -> aux rem seen
+    in
+    aux (NMap.singleton a false) NMap.empty
+
+  let closure x graph =
+    let rec aux rem seen =
+      if NSet.is_empty rem then seen
+      else
+        let x = NSet.choose rem in
+        let rem = NSet.remove x rem in
+        if NSet.mem x seen then 
+          aux rem seen
+        else
+          let seen = NSet.add x seen in
+          let next = try NMap.find x graph with Not_found -> NSet.empty in
+          let rem = NSet.union next rem in
+          aux rem seen
+    in
+    aux (NSet.singleton x) NSet.empty
+
+    let empty = { dir = NMap.empty; rev = NMap.empty; }
+
+    (** Online transitive reduction algorithm *)
+    let add_transitive_edge x y graph =
+      if connected x y graph.dir then graph
+      else
+        let dir = add_edge x y graph.dir in
+        let rev = add_edge y x graph.rev in
+        let graph = { dir; rev; } in
+        let ancestors = closure x rev in
+        let descendents = closure y dir in
+        let fold_ancestor a graph =
+          let fold_descendent b graph =
+            let to_remove = has_edge a b graph.dir in
+            let to_remove = to_remove && not (node_equal x a && node_equal y b) in
+            let to_remove = to_remove && connected_through a b x y graph.dir in
+            if to_remove then
+              let dir = remove_edge a b graph.dir in
+              let rev = remove_edge b a graph.rev in
+              { dir; rev; }
+            else graph
+          in
+          NSet.fold fold_descendent descendents graph
+        in
+        NSet.fold fold_ancestor ancestors graph
+
+  let iter f graph =
+    let iter x set = NSet.iter (fun y -> f x y) set in
+    NMap.iter iter graph.dir
+
+end
+
+module Graph =
+struct
+(** Dumping a dependency graph **)
+
+module DAG = DAG(struct type t = string let compare = compare end)
+
+(** TODO: we should share this code with Coqdep_common *)
+let treat_coq_file chan =
+  let buf = Lexing.from_channel chan in
+  let deja_vu_v = ref ([]: string list list)
+  and deja_vu_ml = ref ([] : string list) in
+  let mark_v_done acc str =
+    let seen = List.mem str !deja_vu_v in
+    if not seen then
+      let () = addQueue deja_vu_v str in
+      try
+        let file_str = Hashtbl.find vKnown str in
+        (canonize file_str, !suffixe) :: acc
+      with Not_found -> acc
+    else acc
+  in
+  let rec loop acc =
+    let token = try Some (coq_action buf) with Fin_fichier -> None in
+    match token with
+    | None -> acc
+    | Some action ->
+      let acc = match action with
+      | Require strl ->
+        List.fold_left mark_v_done acc strl
+      | RequireString s ->
+        let str = Filename.basename s in
+        mark_v_done acc [str]
+      | Declare sl ->
+        let declare suff dir s =
+          let base = file_name s dir in
+          let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in
+          (escape base, suff ^ opt)
+        in
+        let decl acc str =
+          let s = basename_noext str in
+          if not (List.mem s !deja_vu_ml) then
+            let () = addQueue deja_vu_ml s in
+            match search_mllib_known s with
+            | Some mldir -> (declare ".cma" mldir s) :: acc
+            | None ->
+              match search_ml_known s with
+              | Some mldir -> (declare ".cmo" mldir s) :: acc
+              | None -> acc
+          else acc
+        in
+        List.fold_left decl acc sl
+      | Load str ->
+        let str = Filename.basename str in
+        let seen = List.mem [str] !deja_vu_v in
+        if not seen then
+          let () = addQueue deja_vu_v [str] in
+          try
+            let file_str = Hashtbl.find vKnown [str] in
+            (canonize file_str, ".v") :: acc
+          with Not_found -> acc
+        else acc
+      | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
+      in
+      loop acc
+  in
+  loop []
+
+let treat_coq_file f =
+  let chan = try Some (open_in f) with Sys_error _ -> None in
+  match chan with
+  | None -> []
+  | Some chan ->
+    try
+      let ans = treat_coq_file chan in
+      let () = close_in chan in
+      ans
+    with Syntax_error (i, j) -> close_in chan; error_cannot_parse f (i, j)
+
+type graph =
+  | Element of string
+  | Subgraph of string * graph list
+
+let rec insert_graph name path graphs = match path, graphs with
+  | [] , graphs -> (Element name) :: graphs
+  | (box :: boxes), (Subgraph (hd, names)) :: tl when hd = box ->
+    Subgraph (hd, insert_graph name boxes names) :: tl
+  | _, hd :: tl -> hd :: (insert_graph name path tl)
+  | (box :: boxes), [] -> [ Subgraph (box, insert_graph name boxes []) ]
+
+let print_graphs chan graph =
+  let rec print_aux name = function
+  | [] -> name
+  | (Element str) :: tl -> fprintf chan "\"%s\";\n" str; print_aux name tl
+  | Subgraph (box, names) :: tl ->
+    fprintf chan "subgraph cluster%n {\nlabel=\"%s\";\n" name box;
+    let name = print_aux (name + 1) names in
+    fprintf chan "}\n"; print_aux name tl
+  in
+  ignore (print_aux 0 graph)
+
+let rec pop_common_prefix = function
+  | [Subgraph (_, graphs)] -> pop_common_prefix graphs
+  | graphs -> graphs
+
+let split_path = Str.split (Str.regexp "/")
+
+let rec pop_last = function
+  | [] -> []
+  | [ x ] -> []
+  | x :: xs -> x :: pop_last xs
+
+let get_boxes path = pop_last (split_path path)
+
+let insert_raw_graph file =
+  insert_graph file (get_boxes file)
+
+let rec get_dependencies name args =
+  let vdep  = treat_coq_file (name ^ ".v") in
+  let fold (deps, graphs, alseen) (dep, _) =
+    let dag = DAG.add_transitive_edge name dep deps in
+    if not (List.mem dep alseen) then
+      get_dependencies dep (dag, insert_raw_graph dep graphs, dep :: alseen)
+    else
+      (dag, graphs, alseen)
+  in
+  List.fold_left fold args vdep
+
+let coq_dependencies_dump chan dumpboxes =
+  let (deps, graphs, _) =
+    List.fold_left (fun ih (name, _) -> get_dependencies name ih)
+    (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu,
+    List.map fst !vAccu) !vAccu
+  in
+  fprintf chan "digraph dependencies {\n"; flush chan;
+  if dumpboxes then print_graphs chan (pop_common_prefix graphs)
+  else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu;
+  DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps;
+  fprintf chan "}\n"
+
+end
+
 let usage () =
   eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\n";
   eprintf " extra options:\n";
   eprintf "  -coqlib dir : set the coq standard library directory\n";
-  eprintf "  -exclude-dir f : skip subdirectories named f during -R search\n";
+  eprintf "  -exclude-dir f : skip subdirectories named 'f' during -R search\n";
+  eprintf "  -dumpgraph f : print a dot dependency graph in file 'f'\n";
   exit 1
 
+let split_period = Str.split (Str.regexp (Str.quote "."))
+
 let rec parse = function
   | "-c" :: ll -> option_c := true; parse ll
   | "-D" :: ll -> option_D := true; parse ll
   | "-w" :: ll -> option_w := true; parse ll
-  | "-boot" :: ll -> Flags.boot := true; parse ll
+  | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
-  | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [ln]; parse ll
+  | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [];
+    add_dir add_known r (split_period ln);
+    parse ll
   | "-I" :: r :: "-as" :: [] -> usage ()
-  | "-I" :: r :: ll -> add_dir add_known r []; parse ll
+  | "-I" :: r :: ll -> add_caml_dir r; parse ll
   | "-I" :: [] -> usage ()
-  | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
+  | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
   | "-R" :: r :: "-as" :: [] -> usage ()
-  | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
+  | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
+  | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll
   | "-R" :: ([] | [_]) -> usage ()
+  | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
+  | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
   | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll
   | "-exclude-dir" :: [] -> usage ()
   | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
-  | "-slash" :: ll -> option_slash := true; parse ll
+  | "-slash" :: ll ->
+    Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
+    parse ll
   | ("-h"|"--help"|"-help") :: _ -> usage ()
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
@@ -194,26 +479,42 @@ let coqdep () =
   parse (List.tl (Array.to_list Sys.argv));
   if not Coq_config.has_natdynlink then option_natdynlk := false;
   (* NOTE: These directories are searched from last to first *)
-  if !Flags.boot then begin
+  if !option_boot then begin
     add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "plugins" ["Coq"]
+    add_rec_dir add_known "plugins" ["Coq"];
+    add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
+    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
   end else begin
+    Envars.set_coqlib ~fail:Errors.error;
     let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
-    if Sys.file_exists user then add_rec_dir add_coqlib_known user [];
-    List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.xdg_dirs;
-    List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath;
+    if Sys.file_exists user then add_dir add_coqlib_known user [];
+    List.iter (fun s -> add_dir add_coqlib_known s [])
+      (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
+    List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath;
   end;
-  List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
-  List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
-  List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu;
+  List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
+  List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu;
+  List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu;
   warning_mult ".mli" iter_mli_known;
   warning_mult ".ml" iter_ml_known;
   if !option_sort then begin sort (); exit 0 end;
   if !option_c && not !option_D then mL_dependencies ();
   if not !option_D then coq_dependencies ();
-  if !option_w || !option_D then declare_dependencies ()
+  if !option_w || !option_D then declare_dependencies ();
+  begin match !option_dump with
+  | None -> ()
+  | Some (box, file) ->
+    let chan = open_out file in
+    try Graph.coq_dependencies_dump chan box; close_out chan
+    with e -> close_out chan; raise e
+  end
 
-let _ = Printexc.catch coqdep ()
+let _ =
+  try
+    coqdep ()
+  with Errors.UserError(s,p) ->
+    let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
+    Pp.msgerrnl pp
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index bcc9f33f..bc3435a6 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,7 +16,6 @@ open Coqdep_common
 *)
 
 let rec parse = function
-  | "-slash" :: ll -> option_slash := true; parse ll
   | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
@@ -25,20 +24,26 @@ let rec parse = function
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
-       add_dir add_known r [];
+       add_caml_dir r;
        norec_dirs:=r::!norec_dirs;
        parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
 let coqdep_boot () =
+  let () = option_boot := true in
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
-  if !option_c then
-    add_rec_dir add_known "." []
+  if !option_c then begin
+    add_rec_dir add_known "." [];
+    add_rec_dir (fun _ -> add_caml_known) "." ["Coq"];
+  end
   else begin
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "plugins" ["Coq"];
+    add_caml_dir "tactics";
+    add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
+    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
   end;
   if !option_c then mL_dependencies ();
   coq_dependencies ()
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 253fb037..2e6a15ce 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -22,8 +22,8 @@ let stdout = Pervasives.stdout
 
 let option_c = ref false
 let option_noglob = ref false
-let option_slash = ref false
 let option_natdynlk = ref true
+let option_boot = ref false
 let option_mldep = ref None
 
 let norec_dirs = ref ([] : string list)
@@ -33,9 +33,19 @@ let suffixe = ref ".vo"
 
 type dir = string option
 
-(* filename for printing *)
-let (//) s1 s2 =
-  if !option_slash then s1^"/"^s2 else Filename.concat s1 s2
+(* Filename.concat but always with a '/' *)
+let is_dir_sep s i =
+  match Sys.os_type with
+  | "Unix" -> s.[i] = '/'
+  | "Cygwin" | "Win32" ->
+    let c = s.[i] in c = '/' || c = '\\' || c = ':'
+  | _ -> assert false
+
+let (//) dirname filename =
+  let l = String.length dirname in
+  if l = 0 || is_dir_sep dirname (l-1)
+  then dirname ^ filename
+  else dirname ^ "/" ^ filename
 
 (** [get_extension f l] checks whether [f] has one of the extensions
     listed in [l]. It returns [f] without its extension, alongside with
@@ -51,7 +61,7 @@ let rec get_extension f = function
 
 let basename_noext filename =
   let fn = Filename.basename filename in
-  try Filename.chop_extension fn with _ -> fn
+  try Filename.chop_extension fn with Invalid_argument _ -> fn
 
 (** ML Files specified on the command line. In the entries:
     - the first string is the basename of the file, without extension nor
@@ -76,10 +86,10 @@ let vAccu   = ref ([] : (string * string) list)
 
 let addQueue q v = q := v :: !q
 
-let safe_hash_add clq q (k,v) =
+let safe_hash_add cmp clq q (k,v) =
   try
     let v2 = Hashtbl.find q k in
-    if v<>v2 then
+    if not (cmp v v2) then
       let rec add_clash = function
           (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
         | cl::cltl -> cl::add_clash cltl
@@ -91,19 +101,24 @@ let safe_hash_add clq q (k,v) =
 
 (** Files found in the loadpaths.
     For the ML files, the string is the basename without extension.
-    To allow ML source filename to be potentially capitalized,
-    we perform a double search.
 *)
 
+let warning_ml_clash x s suff s' suff' =
+  if suff = suff' then
+  eprintf
+    "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
+    (match s with None -> "." | Some d -> d)
+    ((match s' with None -> "." | Some d -> d) // x) suff
+
 let mkknown () =
-  let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in
-  let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s
-  and iter f = Hashtbl.iter f h
+  let h = (Hashtbl.create 19 : (string, dir * string) Hashtbl.t) in
+  let add x s suff =
+    try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff
+    with Not_found -> Hashtbl.add h x (s,suff)
+  and iter f = Hashtbl.iter (fun x (s,_) -> f x s) h
   and search x =
-    try Some (Hashtbl.find h (String.uncapitalize x))
-    with Not_found ->
-      try Some (Hashtbl.find h (String.capitalize x))
-      with Not_found -> None
+    try Some (fst (Hashtbl.find h x))
+    with Not_found -> None
   in add, iter, search
 
 let add_ml_known, iter_ml_known, search_ml_known = mkknown ()
@@ -122,7 +137,7 @@ let error_cannot_parse s (i,j) =
 
 let warning_module_notfound f s =
   eprintf "*** Warning: in file %s, library " f;
-  eprintf "%s.v is required and has not been found in loadpath!\n"
+  eprintf "%s.v is required and has not been found in the loadpath!\n"
     (String.concat "." s);
   flush stderr
 
@@ -142,7 +157,7 @@ let warning_clash file dir =
       let f = Filename.basename f1 in
       let d1 = Filename.dirname f1 in
       let d2 = Filename.dirname f2 in
-      let dl = List.map Filename.dirname (List.rev fl) in
+      let dl = List.rev_map Filename.dirname fl in
       eprintf
         "*** Warning: in file %s, \n    required library %s matches several files in path\n    (found %s.v in "
         file (String.concat "." dir) f;
@@ -265,10 +280,10 @@ let escape =
     Buffer.clear s';
     for i = 0 to String.length s - 1 do
       let c = s.[i] in
-      if c = ' ' or c = '#' or c = ':' (* separators and comments *)
-	or c = '%' (* pattern *)
-	or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *)
-	or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 
+      if c = ' ' || c = '#' || c = ':' (* separators and comments *)
+        || c = '%' (* pattern *)
+	|| c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
+	|| i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 
 	    'A' <= s.[1] && s.[1] <= 'Z' || 
 	    'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
       then begin
@@ -283,13 +298,16 @@ let escape =
     done;
     Buffer.contents s'
 
+let compare_file f1 f2 =
+  absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2)
+
 let canonize f =
   let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
   match List.filter (fun (_,full) -> f' = full) !vAccu with
     | (f,_) :: _ -> escape f
     | _ -> escape f
 
-let rec traite_fichier_Coq verbose f =
+let rec traite_fichier_Coq suffixe verbose f =
   try
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
@@ -305,7 +323,7 @@ let rec traite_fichier_Coq verbose f =
 	          addQueue deja_vu_v str;
                   try
                     let file_str = safe_assoc verbose f str in
-                    printf " %s%s" (canonize file_str) !suffixe
+                    printf " %s%s" (canonize file_str) suffixe
                   with Not_found ->
 		    if verbose && not (Hashtbl.mem coqlibKnown str) then
                       warning_module_notfound f str
@@ -316,7 +334,7 @@ let rec traite_fichier_Coq verbose f =
 	        addQueue deja_vu_v [str];
                 try
                   let file_str = Hashtbl.find vKnown [str] in
-                  printf " %s%s" (canonize file_str) !suffixe
+                  printf " %s%s" (canonize file_str) suffixe
                 with Not_found ->
 		  if not (Hashtbl.mem coqlibKnown [str]) then
 		    warning_notfound f s
@@ -350,7 +368,7 @@ let rec traite_fichier_Coq verbose f =
                   let file_str = Hashtbl.find vKnown [str] in
                   let canon = canonize file_str in
                   printf " %s.v" canon;
-                  traite_fichier_Coq true (canon ^ ".v")
+                  traite_fichier_Coq suffixe true (canon ^ ".v")
                 with Not_found -> ()
        	      end
           | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
@@ -408,7 +426,10 @@ let coq_dependencies () =
        let ename = escape name in
        let glob = if !option_noglob then "" else " "^ename^".glob" in
        printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
-       traite_fichier_Coq true (name ^ ".v");
+       traite_fichier_Coq !suffixe true (name ^ ".v");
+       printf "\n";
+       printf "%s.vio: %s.v" ename ename;
+       traite_fichier_Coq ".vio" true (name ^ ".v");
        printf "\n";
        flush stdout)
     (List.rev !vAccu)
@@ -418,18 +439,28 @@ let rec suffixes = function
   | [name] -> [[name]]
   | dir::suffix as l -> l::suffixes suffix
 
-let add_known phys_dir log_dir f =
-  match get_extension f [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
+let add_caml_known phys_dir _ f =
+  let basename,suff =
+    get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in
+  match suff with
+    | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+    | ".mli" -> add_mli_known basename (Some phys_dir) suff
+    | ".mllib" -> add_mllib_known basename (Some phys_dir) suff
+    | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
+    | _ -> ()
+
+let add_known recur phys_dir log_dir f =
+  match get_extension f [".v";".vo"] with
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
-	let paths = suffixes name in
+	let paths = if recur then suffixes name else [name] in
 	List.iter
-	  (fun n -> safe_hash_add clash_v vKnown (n,file)) paths
-    | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir)
-    | (basename,".mli") -> add_mli_known basename (Some phys_dir)
-    | (basename,".mllib") -> add_mllib_known basename (Some phys_dir)
-    | (basename,".mlpack") -> add_mlpack_known basename (Some phys_dir)
+	  (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths
+    | (basename,".vo") when not(!option_boot) ->
+        let name = log_dir@[basename] in
+	let paths = if recur then suffixes name else [name] in
+        List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 (* Visits all the directories under [dir], including [dir],
@@ -456,11 +487,18 @@ let rec add_directory recur add_file phys_dir log_dir =
     done
   with End_of_file -> closedir dirh
 
+(** -Q semantic: go in subdirs but only full logical paths are known. *)
 let add_dir add_file phys_dir log_dir =
-  try add_directory false add_file phys_dir log_dir with Unix_error _ -> ()
+  try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> ()
 
+(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
 let add_rec_dir add_file phys_dir log_dir =
-  handle_unix_error (add_directory true add_file phys_dir) log_dir
+  handle_unix_error (add_directory true (add_file true) phys_dir) log_dir
+
+(** -I semantic: do not go in subdirs. *)
+let add_caml_dir phys_dir =
+  handle_unix_error (add_directory true add_caml_known phys_dir) []
+
 
 let rec treat_file old_dirname old_name =
   let name = Filename.basename old_name
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index b2e01f58..71b96ca0 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 val option_c : bool ref
 val option_noglob : bool ref
-val option_slash : bool ref
+val option_boot : bool ref
 val option_natdynlk : bool ref
 val option_mldep : string option ref
 val norec_dirs : string list ref
@@ -23,13 +23,13 @@ val mliAccu : (string * dir) list ref
 val mllibAccu : (string * dir) list ref
 val vAccu : (string * string) list ref
 val addQueue : 'a list ref -> 'a -> unit
-val add_ml_known : string -> dir -> unit
+val add_ml_known : string -> dir -> string -> unit
 val iter_ml_known : (string -> dir -> unit) -> unit
 val search_ml_known : string -> dir option
-val add_mli_known : string -> dir -> unit
+val add_mli_known : string -> dir -> string -> unit
 val iter_mli_known : (string -> dir -> unit) -> unit
 val search_mli_known : string -> dir option
-val add_mllib_known : string -> dir -> unit
+val add_mllib_known : string -> dir -> string -> unit
 val search_mllib_known : string -> dir option
 val vKnown : (string list, string) Hashtbl.t
 val coqlibKnown : (string list, unit) Hashtbl.t
@@ -39,12 +39,15 @@ val canonize : string -> string
 val mL_dependencies : unit -> unit
 val coq_dependencies : unit -> unit
 val suffixes : 'a list -> 'a list list
-val add_known : string -> string list -> string -> unit
+val add_known : bool -> string -> string list -> string -> unit
+val add_caml_known : string -> string list -> string -> unit
 val add_directory :
   bool ->
   (string -> string list -> string -> unit) -> string -> string list -> unit
+val add_caml_dir : string -> unit
 val add_dir :
-  (string -> string list -> string -> unit) -> string -> string list -> unit
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 val add_rec_dir :
-  (string -> string list -> string -> unit) -> string -> string list -> unit
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 val treat_file : dir -> string -> unit
+val error_cannot_parse : string -> int * int -> 'a
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index 4806fbb0..b447030a 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 2cdc6b2e..8ecc419c 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -18,13 +18,11 @@
   type coq_token =
     | Require of qualid list
     | RequireString of string
-    | Declare of string list (* Names are assumed to be uncapitalized *)
+    | Declare of string list
     | Load of string
     | AddLoadPath of string
     | AddRecLoadPath of string * qualid
 
-  let comment_depth = ref 0
-
   exception Fin_fichier
   exception Syntax_error of int*int
 
@@ -49,6 +47,11 @@
 
   let syntax_error lexbuf =
     raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+
+  (** This is the prefix that should be pre-prepended to files due to the use
+   ** of [From], i.e. [From Xxx... Require ...]
+   **)
+  let from_pre_ident = ref None
 }
 
 let space = [' ' '\t' '\n' '\r']
@@ -79,29 +82,72 @@ let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
   | "Require" space+
-      { require_file lexbuf }
-  | "Require" space+ "Export" space+
-      { require_file lexbuf}
-  | "Require" space+ "Import" space+
-      { require_file lexbuf}
+      { require_modifiers lexbuf }
   | "Local"? "Declare" space+ "ML" space+ "Module" space+
-      { mllist := []; modules lexbuf}
+      { mllist := []; modules lexbuf }
   | "Load" space+
       { load_file lexbuf }
   | "Add" space+ "LoadPath" space+
       { add_loadpath lexbuf }
+  | "Time" space+
+      { coq_action lexbuf }
+  | "Timeout" space+ ['0'-'9']+ space+
+      { coq_action lexbuf }
+  | "From" space+
+      { from_rule lexbuf }
   | space+
       { coq_action lexbuf }
   | "(*"
-      { comment_depth := 1; comment lexbuf; coq_action lexbuf }
+      { comment lexbuf; coq_action lexbuf }
   | eof
       { raise Fin_fichier}
   | _
       { skip_to_dot lexbuf; coq_action lexbuf }
 
+and from_rule = parse
+  | "(*"
+      { comment lexbuf; from_rule lexbuf }
+  | space+
+      { from_rule lexbuf }
+  | coq_ident
+      { module_current_name := [Lexing.lexeme lexbuf];
+	from_pre_ident := Some (coq_qual_id_tail lexbuf);
+	module_names := [];
+	consume_require lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { syntax_error lexbuf }
+
+and require_modifiers = parse
+  | "(*"
+      { comment lexbuf; require_modifiers lexbuf }
+  | "Import" space+
+      { require_file lexbuf }
+  | "Export" space+
+      { require_file lexbuf }
+  | space+
+      { require_modifiers lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { backtrack lexbuf ; require_file lexbuf }
+
+and consume_require = parse
+  | "(*"
+      { comment lexbuf; consume_require lexbuf }
+  | space+
+      { consume_require lexbuf }
+  | "Require" space+
+      { require_modifiers lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { syntax_error lexbuf }
+
 and add_loadpath = parse
   | "(*"
-      { comment_depth := 1; comment lexbuf; add_loadpath lexbuf }
+      { comment lexbuf; add_loadpath lexbuf }
   | space+
       { add_loadpath lexbuf }
   | eof
@@ -112,7 +158,7 @@ and add_loadpath = parse
 
 and add_loadpath_as = parse
   | "(*"
-      { comment_depth := 1; comment lexbuf; add_loadpath_as lexbuf }
+      { comment lexbuf; add_loadpath_as lexbuf }
   | space+
       { add_loadpath_as lexbuf }
   | "as"
@@ -148,8 +194,8 @@ and caml_action = parse
       { caml_action lexbuf }
   | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
       { caml_action lexbuf }
-  | "(*" (* "*)" *)
-      { comment_depth := 1; comment lexbuf; caml_action lexbuf }
+  | "(*"
+      { comment lexbuf; caml_action lexbuf }
   | "#" | "&"  | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".."
    | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|"
    | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-"
@@ -174,11 +220,10 @@ and caml_action = parse
   | _ { caml_action lexbuf }
 
 and comment = parse
-  | "(*" (* "*)" *)
-      { comment_depth := succ !comment_depth; comment lexbuf }
+  | "(*"
+      { comment lexbuf; comment lexbuf }
   | "*)"
-      { comment_depth := pred !comment_depth;
-        if !comment_depth > 0 then comment lexbuf }
+      { () }
   | "'" [^ '\\' '\''] "'"
       { comment lexbuf }
   | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'"
@@ -218,7 +263,7 @@ and load_file = parse
 
 and require_file = parse
   | "(*"
-      { comment_depth := 1; comment lexbuf; require_file lexbuf }
+      { comment lexbuf; require_file lexbuf }
   | space+
       { require_file lexbuf }
   | coq_ident
@@ -226,7 +271,12 @@ and require_file = parse
         module_names := [coq_qual_id_tail lexbuf];
         let qid = coq_qual_id_list lexbuf in
         parse_dot lexbuf;
-        Require qid }
+	match !from_pre_ident with
+	  None ->
+          Require qid
+	| Some from ->
+	  (from_pre_ident := None ;
+	   Require (List.map (fun x -> from @ x) qid)) }
   | '"' [^'"']* '"' (*'"'*)
       { let s = Lexing.lexeme lexbuf in
         parse_dot lexbuf;
@@ -248,7 +298,7 @@ and parse_dot = parse
 
 and coq_qual_id = parse
   | "(*"
-      { comment_depth := 1; comment lexbuf; coq_qual_id lexbuf }
+      { comment lexbuf; coq_qual_id lexbuf }
   | space+
       { coq_qual_id lexbuf }
   | coq_ident
@@ -264,7 +314,7 @@ and coq_qual_id = parse
 
 and coq_qual_id_tail = parse
   | "(*"
-      { comment_depth := 1; comment lexbuf; coq_qual_id_tail lexbuf }
+      { comment lexbuf; coq_qual_id_tail lexbuf }
   | space+
       { coq_qual_id_tail lexbuf }
   | coq_field
@@ -281,7 +331,7 @@ and coq_qual_id_tail = parse
 
 and coq_qual_id_list = parse
   | "(*"
-      { comment_depth := 1; comment lexbuf; coq_qual_id_list lexbuf }
+      { comment lexbuf; coq_qual_id_list lexbuf }
   | space+
       { coq_qual_id_list lexbuf }
   | coq_ident
@@ -299,8 +349,7 @@ and modules = parse
   | space+
       { modules lexbuf }
   | "(*"
-      { comment_depth := 1; comment lexbuf;
-        modules lexbuf }
+      { comment lexbuf; modules lexbuf }
   | '"' [^'"']* '"'
       { let lex = (Lexing.lexeme lexbuf) in
 	let str = String.sub lex 1 (String.length lex - 2) in
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 6a44684d..c3db3a26 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 9d3593ea..46005741 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 443edc0b..de7290a4 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -25,12 +25,14 @@ let out_to = ref MultFiles
 
 let out_channel = ref stdout
 
+let ( / ) = Filename.concat
+
 let coqdoc_out f =
   if !output_dir <> "" && Filename.is_relative f then
     if not (Sys.file_exists !output_dir) then
       (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
     else
-      Filename.concat !output_dir f
+      !output_dir / f
   else
     f
 
@@ -71,17 +73,19 @@ let normalize_filename f =
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
-  let file = "states/initial.coq" in
+  let file = "theories/Init/Prelude.vo" in
   match Coq_config.coqlib with
-    | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
-      coqlib
+    | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
     | Some _ | None ->
       let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
       let prefix = Filename.dirname coqbin in
-      let rpath = if Coq_config.local then [] else
-	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-      let coqlib = List.fold_left Filename.concat prefix rpath in
-      if Sys.file_exists (Filename.concat coqlib file) then coqlib
+      let rpath =
+        if Coq_config.local then []
+        else if Coq_config.arch_is_win32 then ["lib"]
+        else ["lib/coq"]
+      in
+      let coqlib = List.fold_left (/) prefix rpath in
+      if Sys.file_exists (coqlib / file) then coqlib
       else prefix
 
 let header_trailer = ref true
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index ccd285f1..dbc930f5 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -75,7 +75,7 @@ h4.section {
                    padding-top: 0px; 
                    padding-bottom: 0px; 
                    font-size : 100%;
-                   font-style : bold;
+                   font-weight : bold;
                    text-decoration : underline;
  }
 
@@ -86,8 +86,7 @@ h4.section {
              max-width: 40em;
              color: black;
 	     padding: 10px;
-             background-color: #90bdff;
-             border-style: plain}
+             background-color: #90bdff }
 
 .inlinecode { 
     display: inline;
@@ -160,8 +159,65 @@ tr.infrulemiddle hr {
 #footer { font-size: 65%;
           font-family: sans-serif; }
 
+/* Identifiers: <span class="id" title="...">) */
+
 .id { display: inline; }
 
+.id[title="constructor"] {
+    color: rgb(60%,0%,0%);
+}
+
+.id[title="var"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="variable"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="definition"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="abbreviation"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="lemma"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="instance"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="projection"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="method"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="inductive"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="record"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="class"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="keyword"] {
+ color : #cf1d1d;
+/*     color: black; */
+}
+
+/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */
+
 .id[type="constructor"] { 
     color: rgb(60%,0%,0%);
 }
@@ -261,7 +317,6 @@ tr.infrulemiddle hr {
 #index #footer {
     position: absolute;
     bottom: 0;
-    text-align: bottom;
 }
 
 .paragraph {
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 9de9a38f..f49f9f00 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -1,5 +1,5 @@
 
-% This is coqdoc.sty, by Jean-Christophe Filliâtre
+% This is coqdoc.sty, by Jean-Christophe Filliâtre
 % This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc)
 %
 % You can modify the following macros to customize the appearance
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 390e61d2..4e132ba0 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Index
-
 val coq_file : string -> Cdglobals.coq_module -> unit
 val detect_subtitle : string -> Cdglobals.coq_module -> string option
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 300d104c..edf7ee8e 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,13 +12,6 @@
   open Printf
   open Lexing
 
-  (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *)
-  let new_line lexbuf =
-    let pos = lexbuf.lex_curr_p in
-      lexbuf.lex_curr_p <- { pos with
-	pos_lnum = pos.pos_lnum + 1;
-	pos_bol = pos.pos_cnum }
-
   (* A list function we need *)
   let rec take n ls =
     if n = 0 then [] else
@@ -75,7 +68,6 @@
   let brackets = ref 0
   let comment_level = ref 0
   let in_proof = ref None
-  let in_emph = ref false
 
   let in_env start stop = 
     let r = ref false in
@@ -102,8 +94,6 @@
             let length_skip = 1 + String.length s1 in
               lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip
 
-  let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
-
   (* saving/restoring the PP state *)
 
   type state = {
@@ -127,8 +117,6 @@
 
   let without_light = without_ref Cdglobals.light
 
-  let show_all f = without_gallina (without_light f)
-
   let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
   let end_show () = restore_state ()
 
@@ -251,14 +239,6 @@
     with _ ->
       ()
 
-  let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
-  let extract_ident s =
-    assert (String.length s >= 3);
-    if Str.string_match extract_ident_re s 0 then
-      Str.matched_group 1 s
-    else
-      String.sub s 1 (String.length s - 3)
-
   let output_indented_keyword s lexbuf =
     let nbsp,isp = count_spaces s in
     Output.indentation nbsp;
@@ -282,10 +262,8 @@ let firstchar =
   '\195' ['\152'-'\182'] |
   '\195' ['\184'-'\191'] |
   (* utf-8 letterlike symbols *)
-  (* '\206' ([ '\145' - '\183'] | '\187') | *)
-  (* '\xCF' [ '\x00' - '\xCE' ] |  *)
-  (* utf-8 letterlike symbols *)
-  '\206' (['\145'-'\161'] | ['\163'-'\187']) |
+  '\206' (['\145'-'\161'] | ['\163'-'\191']) |
+  '\207' (['\145'-'\191']) |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
@@ -333,6 +311,7 @@ let def_token =
   | "Boxed"
   | "CoFixpoint"
   | "Record"
+  | "Variant"
   | "Structure"
   | "Scheme"
   | "Inductive"
@@ -345,7 +324,7 @@ let def_token =
 let decl_token =
   "Hypothesis"
   | "Hypotheses"
-  | "Parameter"
+  | "Parameter" 's'?
   | "Axiom" 's'?
   | "Conjecture"
 
@@ -626,7 +605,7 @@ and coq = parse
 	    end
 	  else
 	    begin
-	      Output.ident s (lexeme_start lexbuf);
+	      Output.ident s None;
 	      let eol=body lexbuf in
 		if eol then coq_bol lexbuf else coq lexbuf
 	    end }
@@ -656,17 +635,17 @@ and coq = parse
 	if eol then coq_bol lexbuf else coq lexbuf }
   | gallina_kw
       { let s = lexeme lexbuf in
-	  Output.ident s (lexeme_start lexbuf);
+	  Output.ident s None;
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | notation_kw
       { let s = lexeme lexbuf in
-	Output.ident s (lexeme_start lexbuf);
+	Output.ident s None;
 	let eol= start_notation_string lexbuf in
 	if eol then coq_bol lexbuf else coq lexbuf }
   | prog_kw
       { let s = lexeme lexbuf in
-	  Output.ident s (lexeme_start lexbuf);
+	  Output.ident s None;
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | space+ { Output.char ' '; coq lexbuf }
@@ -914,11 +893,15 @@ and doc indents = parse
 and escaped_math_latex = parse
   | "$" { Output.stop_latex_math () }
   | eof { Output.stop_latex_math () }
+  | "*)"
+        { Output.stop_latex_math (); backtrack lexbuf }
   | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
 
 and escaped_latex = parse
   | "%" { () }
   | eof { () }
+  | "*)"
+        { backtrack lexbuf }
   | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
 
 and escaped_html = parse
@@ -928,12 +911,15 @@ and escaped_html = parse
   | "##"
         { Output.html_char '#'; escaped_html lexbuf }
   | eof { () }
+  | "*)"
+        { backtrack lexbuf }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
 and verbatim inline = parse
   | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | ">>" { Output.stop_verbatim inline }
+  | "*)" { Output.stop_verbatim inline; backtrack lexbuf }
   | eof { Output.stop_verbatim inline }
   | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
 
@@ -953,11 +939,11 @@ and escaped_coq = parse
   | "]"
       { decr brackets;
 	if !brackets > 0 then
-	  (Output.sublexer ']' (lexeme_start lexbuf); escaped_coq lexbuf)
+	  (Output.sublexer_in_doc ']'; escaped_coq lexbuf)
 	else Tokens.flush_sublexer () }
   | "["
       { incr brackets;
-        Output.sublexer '[' (lexeme_start lexbuf); escaped_coq lexbuf }
+        Output.sublexer_in_doc '['; escaped_coq lexbuf }
   | "(*"
       { Tokens.flush_sublexer (); comment_level := 1;
         ignore (comment lexbuf); escaped_coq lexbuf }
@@ -967,7 +953,7 @@ and escaped_coq = parse
       { Tokens.flush_sublexer () }
   | (identifier '.')* identifier
       { Tokens.flush_sublexer();
-        Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+        Output.ident (lexeme lexbuf) None;
         escaped_coq lexbuf }
   | space_nl*
       { let str = lexeme lexbuf in
@@ -979,7 +965,7 @@ and escaped_coq = parse
                                         else Output.start_inline_coq ());
           escaped_coq lexbuf }
   | _ 
-      { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
+      { Output.sublexer_in_doc (lexeme_char lexbuf 0);
         escaped_coq lexbuf }
 
 (*s Coq "Comments" command. *)
@@ -1078,7 +1064,7 @@ and body_bol = parse
   | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
 
 and body = parse
-  | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf}
+  | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
   | nl+ space* "]]" space* nl
       { Tokens.flush_sublexer();
         if not !formatted then
@@ -1147,11 +1133,11 @@ and body = parse
 	     else body lexbuf }
   | "where" 
       { Tokens.flush_sublexer();
-        Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+        Output.ident (lexeme lexbuf) None;
 	start_notation_string lexbuf }
   | identifier
       { Tokens.flush_sublexer();
-        Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+        Output.ident (lexeme lexbuf) (Some (lexeme_start lexbuf));
 	body lexbuf }
   | ".."
       { Tokens.flush_sublexer(); Output.char '.'; Output.char '.';
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8170e173..4a5ff592 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Filename
-open Lexing
 open Printf
 open Cdglobals
 
@@ -36,7 +34,6 @@ type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
 
-let current_type : entry_type ref = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
@@ -95,9 +92,6 @@ let empty_stack = []
 let module_stack = ref empty_stack
 let section_stack = ref empty_stack
 
-let init_stack () =
-  module_stack := empty_stack; section_stack := empty_stack
-
 let push st p = st := p::!st
 let pop st =
   match !st with
@@ -109,27 +103,6 @@ let head st =
     | [] -> ""
     | x::_ -> x
 
-let begin_module m = push module_stack m
-let begin_section s = push section_stack s
-
-let end_block id =
-  (** determines if it ends a module or a section and pops the stack *)
-  if ((String.compare (head !module_stack) id ) == 0) then
-    pop module_stack
-  else if ((String.compare (head !section_stack) id) == 0) then
-    pop section_stack
-  else
-    ()
-
-let make_fullid id =
-  (** prepends the current module path to an id *)
-  let path = string_of_stack !module_stack in
-    if String.length path > 0 then
-      path ^ "." ^ id
-    else
-      id
-
-
 (* Coq modules *)
 
 let split_sp s =
@@ -158,7 +131,7 @@ let find_external_library logicalpath =
   let rec aux = function
     | [] -> raise Not_found
     | (l,u)::rest ->
-        if String.length logicalpath > String.length l &
+        if String.length logicalpath > String.length l &&
           String.sub logicalpath 0 (String.length l + 1) = l ^"."
         then u
         else aux rest
@@ -208,10 +181,6 @@ let sort_entries el =
 
 let display_letter c = if c = '*' then "other" else String.make 1 c
 
-let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
-let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
 let type_name = function
   | Library ->
       let ln = !lib_name in
@@ -304,9 +273,9 @@ let type_of_string = function
   | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
   | "ex" | "scheme" -> Definition
   | "prf" | "thm" -> Lemma
-  | "ind" | "coind" -> Inductive
+  | "ind" | "variant" | "coind" -> Inductive
   | "constr" -> Constructor
-  | "rec" | "corec" -> Record
+  | "indrec" | "rec" | "corec" -> Record
   | "proj" -> Projection
   | "class" -> Class
   | "meth" -> Method
@@ -319,7 +288,7 @@ let type_of_string = function
   | "mod" | "modtype" -> Module
   | "tac" -> TacticDefinition
   | "sec" -> Section
-  | s -> raise (Invalid_argument ("type_of_string:" ^ s))
+  | s -> invalid_arg ("type_of_string:" ^ s)
 
 let ill_formed_glob_file f =
   eprintf "Warning: ill-formed file %s (links will not be available)\n" f
@@ -370,9 +339,6 @@ let read_glob vfile f =
 		    done)
 	       with _ -> ())
 	  | _ ->
-	      try Scanf.sscanf s "not %d %s %s"
-		(fun loc sp id -> add_def loc loc (type_of_string "not") sp id)
-	      with Scanf.Scan_failure _ ->
 	      try Scanf.sscanf s "%s %d:%d %s %s"
 		(fun ty loc1 loc2 sp id ->
                   add_def loc1 loc2 (type_of_string ty) sp id)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 4c1a445c..69b4e4da 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 59d1ac87..9531cd2b 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -60,6 +60,7 @@ let usage () =
   prerr_endline "  --boot               run in boot mode";
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
+  prerr_endline "  -Q <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  --latin1             set ISO-8859-1 input language";
   prerr_endline "  --utf8               set UTF-8 input language";
   prerr_endline "  --charset <string>   set HTML charset";
@@ -320,6 +321,10 @@ let parse () =
 	add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
 	usage ()
+    | "-Q" :: path :: log :: rem ->
+	add_path path log; parse_rec rem
+    | "-Q" :: ([] | [_]) ->
+	usage ()
     | ("-glob-from" | "--glob-from") :: f :: rem ->
 	glob_source := GlobFile f; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
@@ -445,7 +450,7 @@ let gen_mult_files l =
       if (!header_trailer) then Output.trailer ();
       close_out_file()
     end
-      (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
+    (* NB: for latex and texmacs, a separated toc or index is meaningless... *)
 
 let read_glob_file vfile f =
   try Index.read_glob vfile f
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2d29c447..ae6e6388 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -41,7 +41,7 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
-      "Search"; "SearchAbout"; "SearchRewrite";
+      "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
@@ -50,6 +50,7 @@ let is_keyword =
       "subgoal"; "subgoals"; "vm_compute";
       "Opaque"; "Transparent"; "Time";
       "Extraction"; "Extract";
+      "Variant";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -59,7 +60,7 @@ let is_keyword =
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
       "fix"; "cofix";
       (* Ltac *)
-      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch";
       (* Notations *)
       "level"; "associativity"; "no"
        ]
@@ -210,6 +211,7 @@ module Latex = struct
       printf "\\usepackage{fullpage}\n";
       printf "\\usepackage{coqdoc}\n";
       printf "\\usepackage{amsmath,amssymb}\n";
+      printf "\\usepackage{url}\n";
       (match !toc_depth with
        | None -> ()
        | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n);
@@ -383,6 +385,14 @@ module Latex = struct
     end;
     last_was_in := false
 
+  let sublexer_in_doc c =
+    if c = '*' && !last_was_in then begin
+      Tokens.flush_sublexer ();
+      output_char '*'
+    end else
+      Tokens.output_tagged_symbol_char None c;
+    last_was_in := false
+
   let initialize () =
     initialize_tex_html ();
     Tokens.token_tree := token_tree_latex;
@@ -399,8 +409,11 @@ module Latex = struct
   let ident s loc =
     last_was_in := s = "in";
     try
-      let tag = Index.find (get_module false) loc in
-      reference (translate s) tag
+      match loc with
+      | None -> raise Not_found
+      | Some loc ->
+          let tag = Index.find (get_module false) loc in
+          reference (translate s) tag
     with Not_found ->
       if is_tactic s then
 	printf "\\coqdoctac{%s}" (translate s)
@@ -522,8 +535,8 @@ module Html = struct
 	  printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
 	  printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
 	  printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
-	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
-	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
+	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\" />\n" !charset;
+	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\" />\n";
 	  printf "<title>%s</title>\n</head>\n\n" !page_title;
 	  printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
 	  printf "<div id=\"main\">\n\n"
@@ -558,7 +571,7 @@ module Html = struct
           printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true)
     end
 
-  let indentation n = for i = 1 to n do printf "&nbsp;" done
+  let indentation n = for _i = 1 to n do printf "&nbsp;" done
 
   let line_break () = printf "<br/>\n"
 
@@ -573,9 +586,6 @@ module Html = struct
     | '&' -> printf "&amp;"
     | c -> output_char c
 
-  let raw_string s =
-    for i = 0 to String.length s - 1 do char s.[i] done
-
   let escaped =
     let buff = Buffer.create 5 in
     fun s ->
@@ -585,10 +595,24 @@ module Html = struct
 	| '<' -> Buffer.add_string buff "&lt;"
 	| '>' -> Buffer.add_string buff "&gt;"
 	| '&' -> Buffer.add_string buff "&amp;"
+        | '\'' -> Buffer.add_string buff "&acute;"
+        | '\"' -> Buffer.add_string buff "&quot;"
 	| c -> Buffer.add_char buff c
       done;
       Buffer.contents buff
 
+  let sanitize_name s =
+    let rec loop esc i =
+      if i < 0 then if esc then escaped s else s
+      else match s.[i] with
+      | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1)
+      | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1)
+      | _ ->
+        (* This name contains complex characters:
+           this is probably a notation string, we simply hash it. *)
+        Digest.to_hex (Digest.string s)
+    in loop false (String.length s - 1)
+
   let latex_char _ = ()
   let latex_string _ = ()
 
@@ -618,19 +642,19 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External m when !externals ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External _ | Unknown ->
-	printf "<span class=\"id\" type=\"%s\">%s</span>" typ s
+	printf "<span class=\"id\" title=\"%s\">%s</span>" typ s
 
   let reference s r =
     match r with
     | Def (fullid,ty) ->
-	printf "<a name=\"%s\">" fullid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
+	printf "<a name=\"%s\">" (sanitize_name fullid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s
     | Ref (m,fullid,ty) ->
 	ident_ref m fullid (type_name ty) s
 
@@ -640,7 +664,7 @@ module Html = struct
     | Some ref -> reference s ref
     | None ->
 	if issymbchar then output_string s
-	else printf "<span class=\"id\" type=\"var\">%s</span>" s
+	else printf "<span class=\"id\" title=\"var\">%s</span>" s
 
   let sublexer c loc =
     let tag =
@@ -648,6 +672,9 @@ module Html = struct
     in
     Tokens.output_tagged_symbol_char tag c
 
+  let sublexer_in_doc c =
+    Tokens.output_tagged_symbol_char None c
+
   let initialize () =
     initialize_tex_html();
     Tokens.token_tree := token_tree_html;
@@ -657,16 +684,20 @@ module Html = struct
     match Tokens.translate s with Some s -> s | None -> escaped s
 
   let keyword s loc = 
-    printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+    printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
 
   let ident s loc =
     if is_keyword s then begin
-      printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+      printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
     end else begin
-      try reference (translate s) (Index.find (get_module false) loc)
+      try
+        match loc with
+        | None -> raise Not_found
+        | Some loc ->
+            reference (translate s) (Index.find (get_module false) loc)
       with Not_found ->
 	if is_tactic s then
-	  printf "<span class=\"id\" type=\"tactic\">%s</span>" (translate s)
+	  printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
 	else
 	  if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
 	  then
@@ -818,7 +849,7 @@ module Html = struct
 	       "[library]", m ^ ".html", t
 	else
 	 sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
-	sprintf "%s.html#%s" m s, t)
+	sprintf "%s.html#%s" m (sanitize_name s), t)
 
   let format_bytype_index = function
     | Library, idx ->
@@ -827,7 +858,7 @@ module Html = struct
 	Index.map
 	  (fun s m ->
 	     let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
-	       (text, sprintf "%s.html#%s" m s, t)) idx
+	       (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx
 
   (* Impression de la table d'index *)
   let print_index_table_item i =
@@ -923,8 +954,6 @@ module TeXmacs = struct
   let (preamble : string Queue.t) =
     in_doc := false; Queue.create ()
 
-  let push_in_preamble s = Queue.add s preamble
-
   let header () =
     output_string
       "(*i This file has been automatically generated with the command  \n";
@@ -989,6 +1018,9 @@ module TeXmacs = struct
   let sublexer c l =
     if !in_doc then Tokens.output_tagged_symbol_char None c else char c
 
+  let sublexer_in_doc c =
+    char c
+
   let initialize () =
     Tokens.token_tree := token_tree_texmacs;
     Tokens.outfun := output_sublexer_string
@@ -1045,8 +1077,6 @@ module TeXmacs = struct
 
   let paragraph () = printf "\n\n"
 
-  let line_break_true () = printf "<format|line break>"
-
   let line_break () = printf "\n"
 
   let empty_line_of_code () = printf "\n"
@@ -1107,12 +1137,13 @@ module Raw = struct
   let stop_quote () = printf "\""
 
   let indentation n =
-      for i = 1 to n do printf " " done
+      for _i = 1 to n do printf " " done
 
   let keyword s loc = raw_ident s
   let ident s loc = raw_ident s
 
   let sublexer c l = char c
+  let sublexer_in_doc c = char c
 
   let initialize () =
     Tokens.token_tree := ref Tokens.empty_ttree;
@@ -1226,6 +1257,7 @@ let char = select Latex.char Html.char TeXmacs.char Raw.char
 let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
+let sublexer_in_doc = select Latex.sublexer_in_doc Html.sublexer_in_doc TeXmacs.sublexer_in_doc Raw.sublexer_in_doc
 let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
 
 let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 40fe69f7..c4628dd8 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -61,8 +61,9 @@ val rule : unit -> unit
 val nbsp : unit -> unit
 val char : char -> unit
 val keyword : string -> loc -> unit
-val ident : string -> loc -> unit
+val ident : string -> loc option -> unit
 val sublexer : char -> loc -> unit
+val sublexer_in_doc : char -> unit
 val initialize : unit -> unit
 
 val proofbox : unit -> unit
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 33560fce..a93ae855 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,15 +9,16 @@
 (* Application of printing rules based on a dictionary specific to the
    target language *)
 
-open Cdglobals
-
 (*s Dictionaries: trees annotated with string options, each node being a map
     from chars to dictionaries (the subtrees). A trie, in other words.
 
     (code copied from parsing/lexer.ml4 for the use of coqdoc, Apr 2010)
 *)
 
-module CharMap = Map.Make (struct type t = char let compare = compare end)
+module CharMap = Map.Make (struct
+  type t = char
+  let compare (x : t) (y : t) = compare x y
+end)
 
 type ttree = {
   node : string option;
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index 898f2b5c..c4fe3bc8 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
new file mode 100644
index 00000000..be796e69
--- /dev/null
+++ b/tools/coqmktop.ml
@@ -0,0 +1,306 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** {1 Coqmktop} *)
+
+(** coqmktop is a script to link Coq, analogous to ocamlmktop.
+   The command line contains options specific to coqmktop, options for the
+   Ocaml linker and files to link (in addition to the default Coq files). *)
+
+(** {6 Utilities} *)
+
+(** Split a string at each blank
+*)
+let split_list =
+  let spaces = Str.regexp "[ \t\n]+" in
+  fun str -> Str.split spaces str
+
+let (/) = Filename.concat
+
+(** Which user files do we support (and propagate to ocamlopt) ?
+*)
+let supported_suffix f = match CUnix.get_extension f with
+  | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
+  | _ -> false
+
+(** From bytecode extension to native
+*)
+let native_suffix f = match CUnix.get_extension f with
+  | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx"
+  | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa"
+  | ".a" -> f
+  | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a")
+
+(** Transforms a file name in the corresponding Caml module name.
+*)
+let module_of_file name =
+  String.capitalize
+    (try Filename.chop_extension name with Invalid_argument _ -> name)
+
+(** Run a command [prog] with arguments [args].
+    We do not use [Sys.command] anymore, see comment in [CUnix.sys_command].
+*)
+let run_command prog args =
+  match CUnix.sys_command prog args with
+  | Unix.WEXITED 127 -> failwith ("no such command "^prog)
+  | Unix.WEXITED n -> n
+  | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n)
+  | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n)
+
+
+
+(** {6 Coqmktop options} *)
+
+let opt        = ref false
+let top        = ref false
+let echo       = ref false
+let no_start   = ref false
+
+let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
+let is_camlp5 = Coq_config.camlp4 = "camlp5"
+
+
+(** {6 Includes options} *)
+
+(** Since the Coq core .cma are given with their relative paths
+    (e.g. "lib/clib.cma"), we only need to include directories mentionned in
+    the temp main ml file below (for accessing the corresponding .cmi). *)
+
+let std_includes basedir =
+  let rebase d = match basedir with None -> d | Some base -> base / d in
+  ["-I"; rebase ".";
+   "-I"; rebase "lib";
+   "-I"; rebase "toplevel";
+   "-I"; rebase "kernel/byterun";
+   "-I"; Envars.camlp4lib () ] @
+  (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
+
+(** For the -R option, visit all directories under [dir] and add
+    corresponding -I to the [opts] option list (in reversed order) *)
+let incl_all_subdirs dir opts =
+  let l = ref opts in
+  let add f = l := f :: "-I" :: !l in
+  let rec traverse dir =
+    if Sys.file_exists dir && Sys.is_directory dir then
+      let () = add dir in
+      let subdirs = try Sys.readdir dir with any -> [||] in
+      Array.iter (fun f -> traverse (dir/f)) subdirs
+  in
+  traverse dir; !l
+
+
+(** {6 Objects to link} *)
+
+(** NB: dynlink is now always linked, it is used for loading plugins
+    and compiled vm code (see native-compiler). We now reject platforms
+    with ocamlopt but no dynlink.cmxa during ./configure, and give
+    instructions there about how to build a dummy dynlink.cmxa,
+    cf. dev/dynlink.ml. *)
+
+(** OCaml + CamlpX libraries *)
+
+let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
+let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"]
+let libobjs = ocaml_libs @ camlp4_libs
+
+(** Toplevel objects *)
+
+let ocaml_topobjs =
+  if is_ocaml4 then
+    ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"]
+  else
+    ["toplevellib.cma"]
+
+let camlp4_topobjs =
+  if is_camlp5 then
+    ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
+  else
+    [ "Camlp4Top.cmo";
+      "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
+      "Camlp4Parsers/Camlp4OCamlParser.cmo";
+      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
+
+let topobjs = ocaml_topobjs @ camlp4_topobjs
+
+(** Coq Core objects *)
+
+let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts)
+let core_objs = split_list Tolink.core_objs
+let core_libs = split_list Tolink.core_libs
+
+(** Build the list of files to link and the list of modules names
+*)
+let files_to_link userfiles =
+  let top = if !top then topobjs else [] in
+  let modules = List.map module_of_file (top @ core_objs @ userfiles) in
+  let objs = libobjs @ top @ core_libs in
+  let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles
+  in (modules, objs')
+
+
+(** {6 Parsing of the command-line} *)
+
+let usage () =
+  prerr_endline "Usage: coqmktop <options> <ocaml options> files\
+\nFlags are:\
+\n  -coqlib dir    Specify where the Coq object files are\
+\n  -camlbin dir   Specify where the OCaml binaries are\
+\n  -camlp4bin dir Specify where the Camlp4/5 binaries are\
+\n  -o exec-file   Specify the name of the resulting toplevel\
+\n  -boot          Run in boot mode\
+\n  -echo          Print calls to external commands\
+\n  -opt           Compile in native code\
+\n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
+\n  -R dir         Add recursively dir to OCaml search path\
+\n";
+  exit 1
+
+let parse_args () =
+  let rec parse (op,fl) = function
+    | [] -> List.rev op, List.rev fl
+
+    (* Directories *)
+    | "-coqlib" :: d :: rem ->
+	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
+    | "-camlbin" :: d :: rem ->
+	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
+    | "-camlp4bin" :: d :: rem ->
+	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
+    | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem
+    | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage ()
+
+    (* Boolean options of coqmktop *)
+    | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
+    | "-opt" :: rem -> opt := true ; parse (op,fl) rem
+    | "-top" :: rem -> top := true ; parse (op,fl) rem
+    | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem
+    | "-echo" :: rem -> echo := true ; parse (op,fl) rem
+    | ("-v8"|"-full" as o) :: rem ->
+	Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem
+
+    (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *)
+    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
+        parse (o::op,fl) rem
+    | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
+	begin
+	  match rem' with
+	    | a :: rem -> parse (a::o::op,fl) rem
+	    | []       -> usage ()
+	end
+
+    | ("-h"|"-help"|"--help") :: _ -> usage ()
+    | f :: rem when supported_suffix f -> parse (op,f::fl) rem
+    | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
+  in
+  parse ([],[]) (List.tl (Array.to_list Sys.argv))
+
+
+(** {6 Temporary main file} *)
+
+(** remove the temporary main file
+*)
+let clean file =
+  let rm f = if Sys.file_exists f then Sys.remove f in
+  let basename = Filename.chop_suffix file ".ml" in
+  if not !echo then begin
+    rm file;
+    rm (basename ^ ".o");
+    rm (basename ^ ".cmi");
+    rm (basename ^ ".cmo");
+    rm (basename ^ ".cmx")
+  end
+
+(** Initializes the kind of loading in the main program
+*)
+let declare_loading_string () =
+  if not !top then
+    "Mltop.remove ();;"
+  else
+    "begin try\
+\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
+\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
+\n         | Toploop.Directive_none f -> f ()\
+\n         | _ -> ()\
+\n       end\
+\n     with\
+\n       | Not_found -> ()\
+\n     end;;\
+\n\
+\n     let ppf = Format.std_formatter;;\
+\n     Mltop.set_top\
+\n       {Mltop.load_obj=\
+\n         (fun f -> if not (Topdirs.load_file ppf f)\
+\n                   then Errors.error (\"Could not load plugin \"^f));\
+\n        Mltop.use_file=Topdirs.dir_use ppf;\
+\n        Mltop.add_dir=Topdirs.dir_directory;\
+\n        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
+\n"
+
+(** create a temporary main file to link
+*)
+let create_tmp_main_file modules =
+  let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
+  try
+    (* Add the pre-linked modules *)
+    output_string oc "List.iter Mltop.add_known_module [\"";
+    output_string oc (String.concat "\";\"" modules);
+    output_string oc "\"];;\n";
+    (* Initializes the kind of loading *)
+    output_string oc (declare_loading_string());
+    (* Start the toplevel loop *)
+    if not !no_start then output_string oc "Coqtop.start();;\n";
+    close_out oc;
+    main_name
+  with reraise ->
+    clean main_name; raise reraise
+
+
+(** {6 Main } *)
+
+let main () =
+  let (options, userfiles) = parse_args () in
+  (* Directories: *)
+  let () = Envars.set_coqlib ~fail:Errors.error in
+  let camlbin = Envars.camlbin () in
+  let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
+  (* Which ocaml compiler to invoke *)
+  let prog = camlbin/(if !opt then "ocamlopt" else "ocamlc") in
+  (* Which arguments ? *)
+  if !opt && !top then failwith "no custom toplevel in native code !";
+  let flags = if !opt then [] else Coq_config.vmbyteflags in
+  let topstart = if !top then [ "topstart.cmo" ] else [] in
+  let (modules, tolink) = files_to_link userfiles in
+  let main_file = create_tmp_main_file modules in
+  try
+    (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
+       - With the coq .cma, we MUST use the -linkall option. *)
+    let args =
+      "-linkall" :: "-rectypes" :: flags @ copts @ options @
+      (std_includes basedir) @ tolink @ [ main_file ] @ topstart
+    in
+    if !echo then begin
+      let command = String.concat " " (prog::args) in
+      print_endline command;
+      print_endline
+	("(command length is " ^
+	    (string_of_int (String.length command)) ^ " characters)");
+      flush Pervasives.stdout
+    end;
+    let exitcode = run_command prog args in
+    clean main_file;
+    exitcode
+  with reraise -> clean main_file; raise reraise
+
+let pr_exn = function
+  | Failure msg -> msg
+  | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err
+  | any -> Printexc.to_string any
+
+let _ =
+  try exit (main ())
+  with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index db927efb..417ec535 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,13 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (* coqwc - counts the lines of spec, proof and comments in Coq sources
- * Copyright (C) 2003 Jean-Christophe Filliâtre *)
+ * Copyright (C) 2003 Jean-Christophe Filliâtre *)
 
 (*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
     It assumes the files to be lexically well-formed. *)
@@ -15,7 +15,6 @@
 (*i*){
 open Printf
 open Lexing
-open Filename
 (*i*)
 
 (*s Command-line options. *)
@@ -96,6 +95,8 @@ let stars = "(*" '*'* "*)"
 let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
 let proof_start =
   "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
+let def_start =
+  "Definition" | "Fixpoint" | "Instance"
 let proof_end =
   ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.'
 
@@ -108,14 +109,10 @@ rule spec = parse
   | '\n'   { newline (); spec lexbuf }
   | space+ | stars
            { spec lexbuf }
-  | proof_start space
+  | proof_start
            { seen_spec := true; spec_to_dot lexbuf; proof lexbuf }
-  | proof_start '\n'
-           { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf }
-  | "Program"? "Definition" space
+  | def_start
            { seen_spec := true; definition lexbuf }
-  | "Program"? "Fixpoint" space
-  	   { seen_spec := true; definition lexbuf }
   | character | _
 	   { seen_spec := true; spec lexbuf }
   | eof    { () }
@@ -134,7 +131,7 @@ and spec_to_dot = parse
 	   { seen_spec := true; spec_to_dot lexbuf }
   | eof    { () }
 
-(*s [definition] scans a definition; passes to [proof] is the body is
+(*s [definition] scans a definition; passes to [proof] if the body is
     absent, and to [spec] otherwise *)
 
 and definition = parse
@@ -160,6 +157,8 @@ and proof = parse
            { proof lexbuf }
   | '\n'   { newline (); proof lexbuf }
   | "Proof" space* '.'
+  | "Proof" space+ "with"
+  | "Proof" space+ "using"
            { seen_proof := true; proof lexbuf }
   | "Proof" space
            { proof_term lexbuf }
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
new file mode 100644
index 00000000..8c089150
--- /dev/null
+++ b/tools/coqworkmgr.ml
@@ -0,0 +1,222 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CoqworkmgrApi
+
+let debug = ref false
+
+type party = {
+          sock     : Unix.file_descr;
+          cout     : out_channel;
+  mutable tokens   : int;
+          priority : Flags.priority;
+}
+
+let answer party msg =
+  output_string party.cout (print_response msg); flush party.cout
+
+let mk_socket_channel () =
+  let open Unix in
+  let s = socket PF_INET SOCK_STREAM 0 in
+  bind s (ADDR_INET (inet_addr_loopback,0));
+  listen s 1;
+  match getsockname s with
+  | ADDR_INET(host, port) ->
+      s, string_of_inet_addr host ^":"^ string_of_int port
+  | _ -> assert false
+
+module Queue : sig
+  type t
+  val is_empty : t -> bool
+  val push : int * party -> t -> unit
+  val pop : t -> int * party
+  val create : unit -> t
+end = struct
+  type t = (int * party) list ref
+  let create () = ref []
+  let is_empty q = !q = []
+  let rec split acc = function
+    | [] -> List.rev acc, []
+    | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l
+    | x :: xs -> split (x :: acc) xs
+  let push (_,{ priority } as item) q =
+    if priority = Flags.Low then q := !q @ [item]
+    else
+      let high, low = split [] !q in
+      q := high @ (item :: low)
+  let pop q = match !q with x :: xs -> q := xs; x | _ -> assert false
+end
+
+let read_fd fd s ~off ~len =
+  let rec loop () =
+    try Unix.read fd s off len
+    with Unix.Unix_error(Unix.EAGAIN,_,_) -> loop ()
+  in 
+    loop ()
+
+let really_read_fd fd s off len =
+  let i = ref 0 in
+  while !i < len do
+    let off = off + !i in
+    let len = len - !i in
+    let r = read_fd fd s ~off ~len in
+    if r = 0 then raise End_of_file;
+    i := !i + r
+  done
+
+let raw_input_line fd =
+  try
+    let b = Buffer.create 80 in
+    let s = String.make 1 '\000' in
+    while s <> "\n" do
+      really_read_fd fd s 0 1;
+      if s <> "\n" && s <> "\r" then Buffer.add_string b s;
+    done;
+    Buffer.contents b
+  with Unix.Unix_error _ -> raise End_of_file
+
+let accept s =
+  let cs, _ = Unix.accept s in
+  let cout = Unix.out_channel_of_descr cs in
+  set_binary_mode_out cout true;
+  match parse_request (raw_input_line cs) with
+  | Hello p -> { sock=cs; cout; tokens=0; priority=p }
+  | _ -> (try Unix.close cs with _ -> ()); raise End_of_file
+
+let parse s = ()
+
+let parties = ref []
+
+let max_tokens = ref 2
+let cur_tokens = ref 0
+
+let queue = Queue.create ()
+
+let rec allocate n party =
+  let extra = min n (!max_tokens - !cur_tokens) in
+  cur_tokens := !cur_tokens + extra;
+  party.tokens <- party.tokens + extra;
+  answer party (Tokens extra)
+
+and de_allocate n party =
+  let back = min party.tokens n in
+  party.tokens <- party.tokens - back;
+  cur_tokens := min (!cur_tokens - back) !max_tokens;
+  eventually_dequeue ()
+
+and eventually_dequeue () =
+  if Queue.is_empty queue || !cur_tokens >= !max_tokens then ()
+  else
+    let req, party = Queue.pop queue in
+    if List.exists (fun { sock } -> sock = party.sock) !parties
+    then allocate req party
+    else eventually_dequeue ()
+
+let chat s =
+  let party =
+    try List.find (fun { sock } -> sock = s) !parties
+    with Not_found -> Printf.eprintf "Internal error"; exit 1 in
+  try
+    match parse_request (raw_input_line party.sock) with
+    | Get n ->
+        if !cur_tokens < !max_tokens then allocate n party     
+        else Queue.push (n,party) queue
+    | TryGet n ->
+        if !cur_tokens < !max_tokens then allocate n party     
+        else answer party Noluck
+    | GiveBack n -> de_allocate n party
+    | Ping ->
+        answer party (Pong (!cur_tokens,!max_tokens,Unix.getpid ()));
+        raise End_of_file
+    | Hello _ -> raise End_of_file
+  with Failure _ | ParseError | Sys_error _ | End_of_file ->
+    (try Unix.close party.sock with _ -> ());
+    parties := List.filter (fun { sock } -> sock <> s) !parties;
+    de_allocate party.tokens party;
+    eventually_dequeue ()
+
+let check_alive s =
+  match CoqworkmgrApi.connect s with
+  | Some s ->
+      let cout = Unix.out_channel_of_descr s in
+      set_binary_mode_out cout true;
+      output_string cout (print_request (Hello Flags.Low)); flush cout;
+      output_string cout (print_request Ping); flush cout;
+      begin match Unix.select [s] [] [] 1.0 with
+      | [s],_,_ ->
+          let cin = Unix.in_channel_of_descr s in
+          set_binary_mode_in cin true;
+          begin match parse_response (input_line cin) with
+          | Pong (n,m,pid) -> n, m, pid
+          | _ -> raise Not_found
+          end
+      | _ -> raise Not_found
+      end
+  | _ -> raise Not_found
+
+let main () =
+  let args = [
+    "-j",Arg.Set_int max_tokens, "max number of concurrent jobs";
+    "-d",Arg.Set debug, "do not detach (debug)"] in
+  let usage =
+    "Prints on stdout an env variable assignement to be picked up by coq\n"^
+    "instances in order to limit the maximum number of concurrent workers.\n"^
+    "The default value is 2.\n"^
+    "Usage:" in
+  Arg.parse args (fun extra ->
+    Arg.usage args ("Unexpected argument "^extra^".\n"^usage))
+    usage;
+  try
+    let sock = Sys.getenv "COQWORKMGR_SOCK" in
+    if !debug then Printf.eprintf "Contacting %s\n%!" sock;
+    let cur, max, pid = check_alive sock in
+    Printf.printf "COQWORKMGR_SOCK=%s\n%!" sock;
+    Printf.eprintf
+      "coqworkmgr already up and running (pid=%d, socket=%s, j=%d/%d)\n%!"
+      pid sock cur max;
+    exit 0
+  with Not_found | Failure _ | Invalid_argument _ | Unix.Unix_error _ ->
+  if !debug then Printf.eprintf "No running instance. Starting a new one\n%!";
+  let master, str = mk_socket_channel () in
+  if not !debug then begin
+    let pid = Unix.fork () in
+    if pid <> 0 then begin
+      Printf.printf "COQWORKMGR_SOCK=%s\n%!" str;
+      exit 0 
+    end else begin
+      ignore(Unix.setsid ());
+      Unix.close Unix.stdin;
+      Unix.close Unix.stdout;
+    end;
+  end else begin
+    Printf.printf "COQWORKMGR_SOCK=%s\n%!" str;
+  end;
+  Sys.catch_break true;
+  try
+    while true do
+      if !debug then
+        Printf.eprintf "Status: #parties=%d tokens=%d/%d \n%!"
+          (List.length !parties) !cur_tokens !max_tokens;
+      let socks = master :: List.map (fun { sock } -> sock) !parties in
+      let r, _, _ = Unix.select socks [] [] (-1.0) in
+      List.iter (fun s ->
+        if s = master then begin
+          try parties := accept master :: !parties
+          with _ -> ()
+        end else chat s)
+      r
+    done;
+    exit 0
+  with Sys.Break ->
+    if !parties <> [] then begin
+      Printf.eprintf "Some coq processes still need me\n%!";
+      exit 1;
+    end else
+      exit 0
+
+let () = main ()
diff --git a/tools/escape_string.ml b/tools/escape_string.ml
deleted file mode 100644
index 50e8faad..00000000
--- a/tools/escape_string.ml
+++ /dev/null
@@ -1 +0,0 @@
-print_string (String.escaped Sys.argv.(1))
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index a7203dc8..c2b12668 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,77 +8,324 @@
 
 (** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
 
-exception Comment
-
-let coqtop = ref (stdin, stdout)
-
-let p = Xml_parser.make ()
-let () = Xml_parser.check_eof p false
-
-let eval_call (call:'a Ide_intf.call) =
-  prerr_endline (Ide_intf.pr_call call);
-  let xml_query = Ide_intf.of_call call in
-  Xml_utils.print_xml (snd !coqtop) xml_query;
-  flush (snd !coqtop);
-  let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
-  let res = Ide_intf.to_answer xml_answer call in
-  prerr_endline (Ide_intf.pr_full_value call res);
-  match res with Interface.Fail _ -> exit 1 | _ -> ()
-
-let commands =
-  [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (0,true,false,s)));
-    "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (0,true,true,s)));
-    "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (0,false,false,s)));
-    "INTERP", (fun s -> eval_call (Ide_intf.interp (0,false,true,s)));
-    "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s)));
-    "GOALS", (fun _ -> eval_call (Ide_intf.goals ()));
-    "HINTS", (fun _ -> eval_call (Ide_intf.hints ()));
-    "GETOPTIONS", (fun _ -> eval_call (Ide_intf.get_options ()));
-    "STATUS", (fun _ -> eval_call (Ide_intf.status ()));
-    "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s));
-    "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s));
-    "#", (fun _ -> raise Comment);
-  ]
-
-let read_eval_print line =
-  let lline = String.length line in
-  let rec find_cmd = function
-    | [] -> prerr_endline ("Error: Unknown API Command :"^line); exit 1
-    | (cmd,fn) :: cmds ->
-      let lcmd = String.length cmd in
-      if lline >= lcmd && String.sub line 0 lcmd = cmd then
-	let arg = try String.sub line (lcmd+1) (lline-lcmd-1) with _ -> ""
-	in fn arg
-      else find_cmd cmds
+let error s =
+  prerr_endline ("fake_id: error: "^s);
+  exit 1
+
+type coqtop = {
+  xml_printer : Xml_printer.t;
+  xml_parser : Xml_parser.t;
+}
+
+let logger level content = prerr_endline content
+
+let base_eval_call ?(print=true) ?(fail=true) call coqtop =
+  if print then prerr_endline (Xmlprotocol.pr_call call);
+  let xml_query = Xmlprotocol.of_call call in
+  Xml_printer.print coqtop.xml_printer xml_query;
+  let rec loop () =
+    let xml = Xml_parser.parse coqtop.xml_parser in
+    if Pp.is_message xml then
+      let message = Pp.to_message xml in
+      let level = message.Pp.message_level in
+      let content = message.Pp.message_content in
+      logger level content;
+      loop ()
+    else if Feedback.is_feedback xml then
+      loop ()
+    else (Xmlprotocol.to_answer call xml)
   in
-  find_cmd commands
+  let res = loop () in
+  if print then prerr_endline (Xmlprotocol.pr_full_value call res);
+  match res with
+  | Interface.Fail (_,_,s) when fail -> error s
+  | Interface.Fail (_,_,s) as x -> prerr_endline s; x
+  | x -> x
+
+let eval_call c q = ignore(base_eval_call c q)
+
+module Parser = struct (* {{{ *)
+
+  exception Err of string
+  exception More
+
+  type token =
+    | Tok of string * string
+    | Top of token list
+
+  type grammar =
+    | Alt of grammar list
+    | Seq of grammar list
+    | Opt of grammar
+    | Item of (string * (string -> token * int))
+
+  let eat_rex x = x, fun s ->
+    if Str.string_match (Str.regexp x) s 0 then begin
+      let m = Str.match_end () in
+      let w = String.sub s 0 m in
+      Tok(x,w), m
+    end else raise (Err ("Regexp "^x^" not found in: "^s))
+
+  let eat_balanced c =
+    let c' = match c with
+      | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in
+    let sc, sc' = String.make 1 c, String.make 1 c' in
+    let name = sc ^ "..." ^ sc' in
+    let unescape s =
+      Str.global_replace (Str.regexp ("\\\\"^sc)) sc
+        (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in
+    name, fun s ->
+    if s.[0] = c then
+      let rec find n m =
+        if String.length s <= m then raise More;
+        if s.[m] = c' then
+          if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1
+          else find (n-1) (m+1)
+        else if s.[m] = c then find (n+1) (m+1)
+        else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then
+          find n (m+2)
+        else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then
+          find n (m+2)
+        else find n (m+1)
+      in find ~-1 0
+    else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
+
+  let eat_blanks s = snd (eat_rex "[ \n\t]*") s
+
+  let s = ref ""
+
+  let parse g ic =
+    let read_more () = s := !s ^ input_line ic ^ "\n" in
+    let ensure_non_empty n = if n = String.length !s then read_more () in
+    let cut_after s n = String.sub s n (String.length s - n) in
+    let rec wrap f n =
+      try
+        ensure_non_empty n;
+        let _, n' = eat_blanks (cut_after !s n) in
+        ensure_non_empty n';
+        let t, m = f (cut_after !s (n+n')) in
+        let _, m' = eat_blanks (cut_after !s (n+n'+m)) in
+        t, n+n'+m+m'
+      with More -> read_more (); wrap f n in
+    let rec aux n g res : token list * int =
+      match g with
+      | Item (_,f) ->
+          let t, n = wrap f n in
+          t :: res, n
+      | Opt g ->
+          (try let res', n = aux n g [] in Top (List.rev res') :: res, n
+          with Err _ -> Top [] :: res, n)
+      | Alt gl ->
+          let rec fst = function
+            | [] -> raise (Err ("No more alternatives for: "^cut_after !s n))
+            | g :: gl ->
+               try aux n g res
+               with Err s -> fst gl in
+          fst gl
+      | Seq gl ->
+          let rec all (res,n) = function
+            | [] -> res, n
+            | g :: gl -> all (aux n g res) gl in
+          all (res,n) gl in
+    let res, n = aux 0 g [] in
+    s := cut_after !s n;
+    List.rev res
+
+  let clean s = Str.global_replace (Str.regexp "\n") "\\n" s
+
+  let rec print g =
+    match g with
+    | Item (s,_) -> Printf.sprintf "%s" (clean s)
+    | Opt g -> Printf.sprintf "[%s]" (print g)
+    | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs))
+    | Seq gs -> String.concat " " (List.map print gs)
+
+  let rec print_toklist = function
+    | [] -> ""
+    | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest
+    | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest
+    | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest
+
+end (* }}} *)
+
+type sentence = {
+  name : string;
+  text : string;
+  edit_id : int;
+}
+
+let doc : sentence Document.document = Document.create ()
+
+let tip_id () =
+  try Document.tip doc
+  with
+  | Document.Empty -> Stateid.initial
+  | Invalid_argument _ -> error "add_sentence on top of non assigned tip"
+
+let add_sentence =
+  let edit_id = ref 0 in
+  fun ?(name="") text ->
+    let tip_id = tip_id () in
+    decr edit_id;
+    Document.push doc { name; text; edit_id = !edit_id };
+    !edit_id, tip_id
+
+let print_document () =
+  let ellipsize s =
+          Str.global_replace (Str.regexp "^[\n ]*") ""
+      (if String.length s > 20 then String.sub s 0 17 ^ "..."
+       else s) in
+  prerr_endline (Pp.string_of_ppcmds
+    (Document.print doc
+      (fun b state_id { name; text } ->
+        Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
+          (if b then "*" else " ")
+          name
+          (Stateid.to_string (Option.default Stateid.dummy state_id))
+          (ellipsize text)))))
+
+(* This module is the logic a GUI has to implement *)
+module GUILogic = struct
+
+  let after_add = function
+    | Interface.Fail (_,_,s) -> error s
+    | Interface.Good (id, (Util.Inl (), _)) ->
+        Document.assign_tip_id doc id
+    | Interface.Good (id, (Util.Inr tip, _)) ->
+        Document.assign_tip_id doc id;
+        Document.unfocus doc;
+        ignore(Document.cut_at doc tip);
+        print_document ()
+  
+  let at id id' _ = Stateid.equal id' id
+  
+  let after_edit_at (id,need_unfocus) = function
+    | Interface.Fail (_,_,s) -> error s
+    | Interface.Good (Util.Inl ()) ->
+        if need_unfocus then Document.unfocus doc;
+        ignore(Document.cut_at doc id);
+        print_document ()
+    | Interface.Good (Util.Inr (stop_id,(start_id,tip))) ->
+        if need_unfocus then Document.unfocus doc;
+        ignore(Document.cut_at doc tip);
+        Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id);
+        ignore(Document.cut_at doc id);
+        print_document ()
+  
+  let get_id_pred pred =
+    try Document.find_id doc pred
+    with Not_found -> error "No state found"
+
+  let get_id id = get_id_pred (fun _ { name } -> name = id)
+  
+  let after_fail coq = function
+    | Interface.Fail (safe_id,_,s) ->
+        prerr_endline "The command failed as expected";
+        let to_id, need_unfocus =
+          get_id_pred (fun id _ -> Stateid.equal id safe_id) in
+        after_edit_at (to_id, need_unfocus)
+          (base_eval_call (Xmlprotocol.edit_at to_id) coq)
+    | Interface.Good _ -> error "The command was expected to fail but did not"
+
+end
+
+open GUILogic
+
+let eval_print l coq =
+  let open Parser in
+  let open Xmlprotocol in
+  (* prerr_endline ("Interpreting: " ^ print_toklist l); *)
+  match l with
+  | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] ->
+      let eid, tip = add_sentence phrase in
+      after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
+  | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] ->
+      let eid, tip = add_sentence ~name phrase in
+      after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
+  | [ Tok(_,"GOALS"); ] ->
+      eval_call (goals ()) coq
+  | [ Tok(_,"FAILGOALS"); ] ->
+      after_fail coq (base_eval_call ~fail:false (goals ()) coq)
+  | [ Tok(_,"EDIT_AT"); Tok(_,id) ] ->
+      let to_id, need_unfocus = get_id id in
+      after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
+  | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
+      eval_call (query (phrase,tip_id())) coq
+  | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
+      let to_id, _ = get_id id in
+      eval_call (query (phrase, to_id)) coq
+  | [ Tok(_,"WAIT") ] ->
+      let phrase = "Stm Wait." in
+      eval_call (query (phrase,tip_id())) coq
+  | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
+      let to_id, _ = get_id id in
+      if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
+      else prerr_endline "Good tip"
+  | Tok("#[^\n]*",_) :: _  -> ()
+  | _ -> error "syntax error"
+
+let grammar =
+  let open Parser in
+  let eat_id = eat_rex "[a-zA-Z_][a-zA-Z0-9_]*" in
+  let eat_phrase = eat_balanced '{' in
+  Alt
+    [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase]
+    ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
+    ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
+    ; Seq [Item (eat_rex "WAIT")]
+    ; Seq [Item (eat_rex "GOALS")]
+    ; Seq [Item (eat_rex "FAILGOALS")]
+    ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
+    ; Item (eat_rex "#[^\n]*")
+    ]
+
+let read_command inc = Parser.parse grammar inc
 
 let usage () =
-  Printf.printf
+  error (Printf.sprintf
     "A fake coqide process talking to a coqtop -ideslave.\n\
-     Usage: %s [<coqtop>]\n\
-     Input syntax is one API call per line, the keyword coming first,\n\
-     with the rest of the line as string argument (e.g. INTERP Check plus.)\n\
-     Supported API keywords are:\n" (Filename.basename Sys.argv.(0));
-  List.iter (fun (s,_) -> Printf.printf "\t%s\n" s) commands;
-  exit 1
+     Usage: %s (file|-) [<coqtop>]\n\
+     Input syntax is the following:\n%s\n"
+     (Filename.basename Sys.argv.(0))
+     (Parser.print grammar))
+
+module Coqide = Spawn.Sync(struct end)
 
 let main =
   Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
-  let coqtop_name = match Array.length Sys.argv with
-    | 1 -> "coqtop"
-    | 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1)
-    | _ -> usage ()
-  in
-  coqtop := Unix.open_process (coqtop_name^" -ideslave");
+  let coqtop_name, coqtop_args, input_file = match Sys.argv with
+    | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+    | [| _; f; ct |] ->
+        let ct = Str.split (Str.regexp " ") ct in
+        List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
+    | _ -> usage () in
+  let inc = if input_file = "-" then stdin else open_in input_file in
+  let coq =
+    let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in
+    let ip = Xml_parser.make (Xml_parser.SChannel cin) in
+    let op = Xml_printer.make (Xml_printer.TChannel cout) in
+    Xml_parser.check_eof ip false;
+    { xml_printer = op; xml_parser = ip } in
+  let init () =
+    match base_eval_call ~print:false (Xmlprotocol.init None) coq with
+    | Interface.Good id ->
+        let dir = Filename.dirname input_file in
+        let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in
+        let eid, tip = add_sentence ~name:"initial" phrase in
+        after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq)
+    | Interface.Fail _ -> error "init call failed" in
+  let finish () =
+    match base_eval_call (Xmlprotocol.status true) coq with
+    | Interface.Good _ -> exit 0
+    | Interface.Fail (_,_,s) -> error s in
+  (* The main loop *)
+  init ();
   while true do
-    let l = try read_line () with End_of_file -> exit 0
-    in
-    try read_eval_print l
-    with
-      | Comment -> ()
-      | e ->
-	prerr_endline ("Uncaught exception" ^ Printexc.to_string e); exit 1
+    let cmd = try read_command inc with End_of_file -> finish () in
+    try eval_print cmd coq
+    with e -> error ("Uncaught exception " ^ Printexc.to_string e)
   done
+
+(* vim:set foldmethod=marker: *)
diff --git a/tools/coq-db.el b/tools/gallina-db.el
index 5081b10b..baabebb1 100644
--- a/tools/coq-db.el
+++ b/tools/gallina-db.el
@@ -1,4 +1,4 @@
-;;; coq-db.el --- coq keywords database utility functions
+;;; gallina-db.el --- coq keywords database utility functions
 ;;
 ;; Author: Pierre Courtieu <courtieu@lri.fr>
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
@@ -48,7 +48,7 @@ Is ok because the longer regexp is recognized first.
 
 If non-nil the optional INSERT-FUN is the function to be called when inserting
 the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This
-allows to write functions asking for more information to assist the user.
+allows writing functions asking for more information to assist the user.
 
 If non-nil the optional HIDE specifies that this form should not appear in the
 menu but only in interactive completions.
@@ -231,9 +231,9 @@ Required so that 'proof-solve-tactics-face is a proper facename")
 
 
 
-(provide 'coq-db)
+(provide 'gallina-db)
 
-;;; coq-db.el ends here
+;;; gallina-db.el ends here
 
 ;** Local Variables: ***
 ;** fill-column: 80 ***
diff --git a/tools/coq-syntax.el b/tools/gallina-syntax.el
index 8630fb3a..c25abece 100644
--- a/tools/coq-syntax.el
+++ b/tools/gallina-syntax.el
@@ -1,14 +1,14 @@
-;; coq-syntax.el Font lock expressions for Coq
+;; gallina-syntax.el Font lock expressions for Coq
 ;; Copyright (C) 1997-2007 LFCS Edinburgh. 
 ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
 
-;; coq-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp
+;; gallina-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp
 
 ;(require 'proof-syntax)
 ;(require 'proof-utils)                  ; proof-locate-executable
-(require 'coq-db)
+(require 'gallina-db)
 
 
 
@@ -360,6 +360,11 @@
     ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t )
     ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t )
     ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t )
+    ("Variant" "indv" "Variant # : # := # : #." t "Variant")
+    ("Variant (2 args)" "indv2" "Variant # : # :=\n| # : #\n| # : #." t )
+    ("Variant (3 args)" "indv3" "Variant # : # :=\n| # : #\n| # : #\n| # : #." t )
+    ("Variant (4 args)" "indv4" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t )
+    ("Variant (5 args)" "indv5" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t )
     ("Let" "Let" "Let # : # := #." t "Let")
     ("Ltac" "ltac" "Ltac # := #" t "Ltac")
     ("Module :=" "mo" "Module # : # := #." t ) ; careful
@@ -618,7 +623,7 @@
 ;; proof-done-advancing-save in generic/proof-script.el) for coq <
 ;; 8.0. It is the test when looking backward the start of the proof.
 ;; It is NOT used for coq > v8.1
-;; (coq-find-and-forget in coq.el uses state numbers, proof numbers and
+;; (coq-find-and-forget in gallina.el uses state numbers, proof numbers and
 ;; lemma names given in the prompt)
 
 ;; compatibility with v8.0, will delete it some day
@@ -950,7 +955,7 @@ Used by `coq-goal-command-p'"
   (modify-syntax-entry ?\' "_")
   (modify-syntax-entry ?\| ".")
 
-;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug
+;; should maybe be "_" but it makes coq-find-and-forget (in gallina.el) bug
   (modify-syntax-entry ?\. ".") 
 
   (condition-case nil
@@ -969,8 +974,8 @@ Used by `coq-goal-command-p'"
  		  1))
  	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
 
-(provide 'coq-syntax)
- ;;; coq-syntax.el ends here
+(provide 'gallina-syntax)
+ ;;; gallina-syntax.el ends here
 
 ; Local Variables: ***
 ; indent-tabs-mode: nil ***
diff --git a/tools/coq.el b/tools/gallina.el
index f4c4b033..cbc13118 100644
--- a/tools/coq.el
+++ b/tools/gallina.el
@@ -1,15 +1,15 @@
-;; coq.el --- Coq mode editing commands for Emacs
+;; gallina.el --- Coq mode editing commands for Emacs
 ;;
 ;; Jean-Christophe Filliatre, march 1995
-;; Honteusement pompé de caml.el, Xavier Leroy, july 1993.
+;; Shamelessly copied from caml.el, Xavier Leroy, july 1993.
 ;;
-;; modified by Marco Maggesi <maggesi@math.unifi.it> for coq-inferior
+;; modified by Marco Maggesi <maggesi@math.unifi.it> for gallina-inferior
 
 ; compatibility code for proofgeneral files
 (require 'coq-font-lock)
 ; ProofGeneral files. remember to remove coq version tests in
-; coq-syntax.el
-(require 'coq-syntax)
+; gallina-syntax.el
+(require 'gallina-syntax)
 
 (defvar coq-mode-map nil
   "Keymap used in Coq mode.")
@@ -137,6 +137,6 @@ Does nothing otherwise."
              (coq-in-indentation))
         (backward-delete-char-untabify coq-mode-indentation))))
 
-;;; coq.el ends here
+;;; gallina.el ends here
 
-(provide 'coq)
+(provide 'gallina)
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 2e9a17f6..279919c5 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index e6f6f4b3..9dd49b90 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -1,13 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 {
- open Lexing
 
  let chan_out = ref stdout
 
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
deleted file mode 100644
index f01b62cc..00000000
--- a/tools/mingwpath.ml
+++ /dev/null
@@ -1,15 +0,0 @@
-(** Mingwpath *)
-
-(** Converts mingw-encoded filenames such as:
-
-      /c/Program Files/Ocaml/bin
-
-    to a more windows-friendly form (but still with / instead of \) :
-
-      c:/Program Files/Ocaml/bin
-
-    This nice hack was suggested by Benjamin Monate (cf bug #2526)
-    to mimic the cygwin-specific tool cygpath
-*)
-
-print_string Sys.argv.(1)
diff --git a/tools/update-require b/tools/update-require
new file mode 100755
index 00000000..cc9a27b8
--- /dev/null
+++ b/tools/update-require
@@ -0,0 +1,103 @@
+#!/bin/sh
+
+# This script fully qualifies all the 'Require' statements of the given
+# targets (or the current directory if none).
+#
+# It assumes that all the prerequisites are already installed. The
+# install location is found using the COQLIB, COQC, COQBIN variables if
+# set, 'coqc' otherwise.
+#
+# Option --exclude can be used to ignore a given user contribution. In
+# particular, it can be used to ignore the current set of files if it
+# happens to be already installed.
+#
+# Option --stdlib can be used to also qualify the files from the standard
+# library.
+
+if test ! "$COQLIB"; then
+  if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
+  if test ! "$COQC"; then COQC=`which ${COQBIN}coqc`; fi
+  COQLIB=`"$COQC" -where`
+fi
+
+stdlib=no
+exclude=""
+
+scan_dir () {
+  (cd $1 ; find $3 -name '*.vo' |
+  sed -e "s,^./,$2,;s,\([^./]*\)/,\1.,g;s,\([^.]*\).vo,\1,")
+}
+
+scan_all_dir () {
+  if test $stdlib = yes; then
+    scan_dir "$COQLIB/theories" "Coq."
+    scan_dir "$COQLIB/plugins" "Coq."
+  fi
+  scan_dir "$COQLIB/user-contrib" "" "$exclude"
+}
+
+create_script () {
+  echo "BEGIN {"
+  scan_all_dir |
+  while read file ; do
+    echo $file | sed -e "s,\(.*\)[.]\([^.]*\),  t[\"\2\"] = \"\1.\2\","
+  done
+  cat <<EOF
+}
+
+\$1 ~ "Require" {
+  for (i = 2; i <= NF; ++i) {
+    if (\$i ~ /[.]\$/) {
+      s = substr(\$i,1,length(\$i)-1)
+      if (t[s]) \$i = t[s] "."
+      break
+    } else if (t[\$i]) \$i = t[\$i]
+  }
+  print
+  next
+}
+
+{ print }
+EOF
+}
+
+usage () {
+  cat <<EOF
+Usage: $0 [OPTION...] [TARGET...]
+The default TARGET is the current directory.
+Available options:
+  --exclude CONTRIB        Do not qualify path to the given CONTRIB
+  --stdlib                 Qualify files from the standard library
+  --help                   Display this message
+EOF
+}
+
+dir=""
+while : ; do
+  case "$1" in
+    "")
+      break;;
+    -h|--help)
+      usage
+      exit 0;;
+    --exclude)
+      exclude="$exclude -path ./$2 -prune -type f -o"
+      shift;;
+    --stdlib)
+      stdlib=yes;;
+    -*)
+      echo "Unknown option $1" 1>&2
+      exit 1;;
+    *)
+      dir="$dir $1";;
+  esac
+  shift
+done
+
+script=`tempfile`
+create_script > $script
+find $dir -name '*.v' |
+while read file; do
+  mv $file $file.bak
+  awk -f $script $file.bak > $file
+done
diff --git a/tools/win32hack.mllib b/tools/win32hack.mllib
deleted file mode 100644
index 42395f65..00000000
--- a/tools/win32hack.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Win32hack_filename
\ No newline at end of file
diff --git a/tools/win32hack_filename.ml b/tools/win32hack_filename.ml
deleted file mode 100644
index 74f70686..00000000
--- a/tools/win32hack_filename.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-(* The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
-   Let's tweak that... *)
-
-let _ = Filename.dir_sep.[0] <- '\\'