Merge branch 'experimental/upstream' into upstream

36 files changed, 1863 insertions, 997 deletions

diff --git a/tools/beautify-archive b/tools/beautify-archive
index ccfeb3db..ccfeb3db 100644..100755
--- a/tools/beautify-archive
+++ b/tools/beautify-archive
diff --git a/tools/compat5.ml b/tools/compat5.ml
new file mode 100644
index 00000000..663f8d44
--- /dev/null
+++ b/tools/compat5.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+   add to gain camlp5 compatibility :-).
+
+   See [compat5.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
new file mode 100644
index 00000000..aabf7288
--- /dev/null
+++ b/tools/compat5.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+    - GEXTEND ... becomes EXTEND ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+  | [< '(KEYWORD "GEXTEND", loc); s >] ->
+    [< '(KEYWORD "EXTEND", loc); my_token_filter s >]
+  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
+  | [< >] -> [< >]
+
+let _ =
+  Token.Filter.define_filter (Gram.get_filter())
+    (fun prev strm -> prev (my_token_filter strm))
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
new file mode 100644
index 00000000..2f104da7
--- /dev/null
+++ b/tools/compat5b.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+   add to gain camlp5 compatibility :-).
+
+   See [compat5b.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
new file mode 100644
index 00000000..f7e08115
--- /dev/null
+++ b/tools/compat5b.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+    - EXTEND ... becomes EXTEND Gram ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+  | [< '(KEYWORD "EXTEND",_ as t); s >] ->
+    [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >]
+  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
+  | [< >] -> [< >]
+
+let _ =
+  Token.Filter.define_filter (Gram.get_filter())
+    (fun prev strm -> prev (my_token_filter strm))
diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el
index 5b88f6a5..8630fb3a 100644
--- a/tools/coq-syntax.el
+++ b/tools/coq-syntax.el
@@ -417,8 +417,10 @@
      ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path")
      ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism")
      ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing")
+     ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor")
      ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If")
      ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let")
+     ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record")
      ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath")
      ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path")
      ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring")
@@ -497,6 +499,7 @@
      ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth")
      ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard")
      ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All")
+     ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records")
      ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit")
      ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions")
      ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations")
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
new file mode 100644
index 00000000..6f0071a4
--- /dev/null
+++ b/tools/coq_makefile.ml
@@ -0,0 +1,720 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \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 *)
+
+let output_channel = ref stdout
+let makefile_name = ref "Makefile"
+let make_name = ref ""
+
+let some_vfile = ref false
+let some_mlfile = ref false
+let some_mlifile = ref false
+let some_ml4file = ref false
+let some_mllibfile = ref false
+let some_mlpackfile = ref false
+
+let print x = output_string !output_channel x
+let printf x = Printf.fprintf !output_channel x
+
+let rec print_list sep = function
+  | [ x ] -> print x
+  | x :: l -> print x; print sep; print_list sep l
+  | [] -> ()
+
+let list_iter_i f =
+  let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1
+
+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;
+  print "# "; print s; print " #\n";
+  print sep2;
+  print sep;
+  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]
+
+[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
+[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\"
+[-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\".
+[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
+[-byte]: compile with byte-code version of coq
+[-opt]: compile with native-code version of coq
+[-arg opt]: send option \"opt\" to coqc
+[-install opt]: where opt is \"user\" to force install into user directory,
+  \"none\" to build a makefile with no install target or
+  \"global\" to force install in $COQLIB directory
+[-f file]: take the contents of file as arguments
+[-o file]: output should go in file file
+	Output file outside the current directory is forbidden.
+[-h]: print this usage summary
+[--help]: equivalent to [-h]\n";
+  exit 1
+
+let is_genrule r =
+    let genrule = Str.regexp("%") in
+      Str.string_match genrule r 0
+
+let string_prefix a b =
+  let rec aux i = try if a.[i] = b.[i] then aux (i+1) else i with |Invalid_argument _ -> i in
+    String.sub a 0 (aux 0)
+
+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] = '/')
+
+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
+  for i = 0 to le - 1 do
+    if pdir.[i] = '.' then pdir.[i] <- '/';
+  done;
+  pdir
+
+let standard opt =
+  print "byte:\n";
+  print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
+  print "opt:\n";
+  if not opt then print "\t@echo \"WARNING: opt is disabled\"\n";
+  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
+    begin
+      let absdir_of_files = List.rev_map
+	(fun x -> Minilib.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
+	if has_inc_i then
+	  begin
+	    printf "%sINC=" var;
+	    List.iter (fun (pdir,absdir) ->
+			 if List.mem absdir absdir_of_files
+			 then printf
+			   "$(filter $(wildcard %s/*),$(%s)) "
+			   pdir var
+		      ) inc_i;
+	    printf "\n";
+	  end;
+      (* Files in the scope of a -R option (assuming they are disjoint) *)
+	list_iter_i (fun i (pdir,ldir,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;
+    end
+
+let install_include_by_root files_var files (inc_i,inc_r) =
+  try
+    (* 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;
+      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 ()
+      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 install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function
+  |Project_file.NoInstall -> ()
+  |is_install ->
+    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;
+      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;
+    List.iter
+      (fun 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 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";
+    List.iter
+      (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n")
+      sds;
+    print "\n";
+  end
+
+let clean sds sps =
+  print "clean:\n";
+  if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile || !some_mlpackfile then begin
+    print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n";
+    print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n";
+    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";
+  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";
+  List.iter
+    (fun (file,_,_) ->
+       if not (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")
+    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")
+    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"
+
+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 "\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
+  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 "\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 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
+  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";
+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"
+  in
+    if !some_mlifile then mli_rules ();
+    if !some_ml4file then ml4_rules ();
+    if !some_mlfile then ml_rules ();
+    if !some_mlfile || !some_ml4file then cmxs_rules ();
+    if !some_mllibfile then mllib_rules ();
+    if !some_mlpackfile then mlpack_rules ();
+    if !some_vfile then v_rules ()
+
+let variables is_install opt (args,defs) =
+  let var_aux (v,def) = print v; print "="; print def; print "\n" in
+    section "Variables definitions.";
+    List.iter var_aux defs;
+    print "\n";
+    if not opt then
+      print "override OPT:=-byte\n"
+    else
+      print "OPT?=\n";
+    begin
+      match args with
+	|[] -> ()
+	|h::t -> print "OTHERFLAGS=";
+	  print h;
+	  List.iter (fun s -> print " ";print s) t;
+	  print "\n";
+    end;
+    (* Coq executables and relative variables *)
+    if !some_vfile || !some_mlpackfile || !some_mllibfile then
+      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";
+    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";
+    List.iter (fun c -> print " \\
+  -I $(COQLIB)plugins/"; print c) 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 "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";
+    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 "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 "endif\n\n"
+      | Project_file.TraditionalInstall ->
+          section "Install Paths.";
+          print "COQLIBINSTALL=${COQLIB}user-contrib\n";
+          print "COQDOCINSTALL=${DOCDIR}user-contrib\n";
+          print "\n"
+      | Project_file.UserInstall ->
+          section "Install Paths.";
+          print "XDG_DATA_HOME?=$(HOME)/.local/share\n";
+          print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
+          print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\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 "# 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
+  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";
+    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";
+    end
+
+let custom sps =
+  let pr_path (file,dependencies,com) =
+    print file; print ": "; print dependencies; print "\n";
+    if com <> "" then (print "\t"; print com); print "\n\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"
+  in
+    if sds <> [] then section "Subdirectories.";
+    List.iter pr_subdir sds
+
+let forpacks l =
+  let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in
+  List.iter (fun it ->
+    let h = Filename.chop_extension it in
+    printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h;
+    printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" (String.capitalize (Filename.basename h));
+    printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h;
+    printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" (String.capitalize (Filename.basename h))
+  ) l
+
+let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc =
+  let decl_var var = function
+    |[] -> ()
+    |l ->
+      printf "%s:=" var; print_list "\\\n  " l; print "\n";
+      printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var
+  in
+  section "Files dispatching.";
+  decl_var "VFILES" vfiles;
+  begin match vfiles with
+    |[] -> ()
+    |l ->
+      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"
+  end;
+  decl_var "ML4FILES" ml4files;
+  decl_var "MLFILES" mlfiles;
+  decl_var "MLPACKFILES" mlpackfiles;
+  decl_var "MLLIBFILES" mllibfiles;
+  decl_var "MLIFILES" mlifiles;
+  let mlsfiles = match ml4files,mlfiles,mlpackfiles with
+    |[],[],[] -> []
+    |[],[],_ -> Printf.eprintf "Mlpack cannot work without ml[4]?"; []
+    |[],ml,[] ->
+      print "ALLCMOFILES:=$(MLFILES:.ml=.cmo)\n";
+      ml
+    |ml4,[],[] ->
+      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo)\n";
+      ml4
+    |ml4,ml,[] ->
+      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n";
+      List.rev_append ml ml4
+    |[],ml,mlpack ->
+      print "ALLCMOFILES:=$(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
+      List.rev_append mlpack ml
+    |ml4,[],mlpack ->
+      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
+      List.rev_append mlpack ml4
+    |ml4,ml,mlpack ->
+      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
+      List.rev_append mlpack (List.rev_append ml ml4) in
+  begin match mlsfiles with
+    |[] -> ()
+    |l ->
+  print "CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))\n";
+      classify_files_by_root "CMOFILES" l inc;
+      print "CMXFILES=$(CMOFILES:.cmo=.cmx)\n";
+      print "OFILES=$(CMXFILES:.cmx=.o)\n";
+  end;
+  begin match mllibfiles with
+    |[] -> ()
+    |l ->
+      print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n";
+	classify_files_by_root "CMAFILES" l inc;
+      print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n";
+  end;
+  begin match mlifiles,mlsfiles with
+    |[],[] -> ()
+    |l,[] ->
+       print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n";
+	classify_files_by_root "CMIFILES" l inc;
+    |[],l ->
+      print "CMIFILES=$(ALLCMOFILES:.cmo=.cmi)\n";
+      classify_files_by_root "CMIFILES" l inc;
+    |l1,l2 ->
+      print "CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n";
+      classify_files_by_root "CMIFILES" (l1@l2) inc;
+  end;
+  begin match mllibfiles,mlsfiles with
+    |[],[] -> ()
+    |l,[] ->
+      print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n";
+      classify_files_by_root "CMXSFILES" l inc;
+    |[],l ->
+      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs)\n";
+      classify_files_by_root "CMXSFILES" l inc;
+    |l1,l2 ->
+      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n";
+      classify_files_by_root "CMXSFILES" (l1@l2) inc;
+  end;
+  print "ifeq '$(HASNATDYNLINK)' 'true'\n";
+  print "HASNATDYNLINK_OR_EMPTY := yes\n";
+  print "else\n";
+  print "HASNATDYNLINK_OR_EMPTY :=\n";
+  print "endif\n\n";
+  section "Definition of the toplevel targets.";
+  print "all: ";
+  if !some_vfile then print "$(VOFILES) ";
+  if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) ";
+  if !some_mllibfile then print "$(CMAFILES) ";
+  if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile
+  then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) ";
+  print_list "\\\n  " other_targets; print "\n\n";
+  if !some_mlifile then
+    begin
+      print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
+      print "\t mkdir $@ || rm -rf $@/*\n";
+      print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
+      print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+    end;
+  if !some_vfile then
+    begin
+      print "spec: $(VIFILES)\n\n";
+      print "gallina: $(GFILES)\n\n";
+      print "html: $(GLOBFILES) $(VFILES)\n";
+      print "\t- mkdir -p html\n";
+      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
+      print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
+      print "\t- mkdir -p html\n";
+      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
+      print "all.ps: $(VFILES)\n";
+      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+      print "all-gal.ps: $(VFILES)\n";
+      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+      print "all.pdf: $(VFILES)\n";
+      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+      print "all-gal.pdf: $(VFILES)\n";
+      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+      print "validate: $(VOFILES)\n";
+      print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n";
+      print "beautify: $(VFILES:=.beautified)\n";
+      print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n";
+      print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n";
+      print "\t@echo \'If there were a problem, execute \"for file in $$(find . -name \\*.v.old -print); do mv $${file} $${file%.old}; done\" in your shell/'\n\n"
+    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
+  main_targets vfiles mlfiles other_targets inc;
+    print ".PHONY: ";
+    print_list " "
+      ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install"
+	:: "userinstall" :: "depend" :: "html" :: "validate" :: sds);
+    print "\n\n";
+    custom sps;
+    subdirs sds;
+    forpacks mlpackfiles
+
+let banner () =
+  print (Printf.sprintf
+"#############################################################################
+##  v      #                   The Coq Proof Assistant                     ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
+##   \\VV/  #                                                               ##
+##    //   #  Makefile automagically generated by coq_makefile V%s ##
+#############################################################################
+
+" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
+
+let warning () =
+  print "# WARNING\n#\n";
+  print "# This Makefile has been automagically generated\n";
+  print "# Edit at your own risks !\n";
+  print "#\n# END OF WARNING\n\n"
+
+let print_list l = List.iter (fun x -> print x; print " ") l
+
+let command_line args =
+  print "#\n# This Makefile was generated by the command line :\n";
+  print "# coq_makefile ";
+  print_list args;
+  print "\n#\n\n"
+
+let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((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
+	&& not_tops mllib && not_tops mlpack) then
+    l
+  else
+    ((".",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
+  let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in
+  if inc_r = [] || List.exists (fun f -> List.mem (Filename.dirname f) inc_top) 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 ")
+
+let check_overlapping_include (_,inc_r) =
+  let pwd = Sys.getcwd () in
+  let rec 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
+	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
+  in aux inc_r
+
+let do_makefile args =
+  let has_file var = function
+    |[] -> var := false
+    |_::_ -> var := true in
+  let (project_file,makefile,is_install,opt),l =
+    try Project_file.process_cmd_line Filename.current_dir_name (None,None,Project_file.UnspecInstall,true) [] args
+    with Project_file.Parsing_error -> usage () in
+  let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs =
+    Project_file.split_arguments l in
+
+  let () = match project_file with |None -> () |Some f -> make_name := f in
+  let () = match makefile with
+    |None -> ()
+    |Some f -> makefile_name := f; output_channel := open_out f in
+  has_file some_vfile v_f; has_file some_mlifile mli_f;
+  has_file some_mlfile ml_f; has_file some_ml4file ml4_f;
+  has_file some_mllibfile mllib_f; has_file some_mlpackfile mlpack_f;
+  let check_dep f =
+    if Filename.check_suffix f ".v" then some_vfile := true
+    else if (Filename.check_suffix f ".mli") then some_mlifile := true
+    else if (Filename.check_suffix f ".ml4") then some_ml4file := true
+    else if (Filename.check_suffix f ".ml") then some_mlfile := true
+    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 check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
+
+  let inc = ensure_root_dir targets inc in
+  if is_install <> Project_file.NoInstall then warn_install_at_root_directory targets inc;
+  check_overlapping_include inc;
+  banner ();
+  header_includes ();
+  warning ();
+  command_line args;
+  parameters ();
+  include_dirs inc;
+  variables is_install opt defs;
+  all_target targets inc;
+  section "Special targets.";
+  standard opt;
+  install targets inc is_install;
+  clean sds sps;
+  make_makefile sds;
+  implicit ();
+  warning ();
+  if not (makefile = None) then close_out !output_channel;
+  exit 0
+
+let main () =
+  let args =
+    if Array.length Sys.argv = 1 then usage ();
+    List.tl (Array.to_list Sys.argv)
+  in
+    do_makefile args
+
+let _ = Printexc.catch main ()
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
deleted file mode 100644
index 50f0344b..00000000
--- a/tools/coq_makefile.ml4
+++ /dev/null
@@ -1,614 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: coq_makefile.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(* créer un Makefile pour un développement Coq automatiquement *)
-
-type target =
-  | ML of string (* ML file : foo.ml -> (ML "foo") *)
-  | V of string  (* V file : foo.v -> (V "foo") *)
-  | Special of string * string * string (* file, dependencies, command *)
-  | Subdir of string
-  | Def of string * string (* X=foo -> Def ("X","foo") *)
-  | Include of string
-  | RInclude of string * string (* -R physicalpath logicalpath *)
-
-let output_channel = ref stdout
-let makefile_name = ref "Makefile"
-let make_name = ref ""
-
-let some_file = ref false
-let some_vfile = ref false
-let some_mlfile = ref false
-
-let opt = ref "-opt"
-let impredicative_set = ref false
-let no_install = ref false
-
-let print x = output_string !output_channel x
-let printf x = Printf.fprintf !output_channel x
-
-let rec print_list sep = function
-  | [ x ] -> print x
-  | x :: l -> print x; print sep; print_list sep l
-  | [] -> ()
-
-let list_iter_i f =
-  let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1
-
-let best_ocamlc =
-  if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc"
-let best_ocamlopt =
-  if Coq_config.best = "opt" then "ocamlopt.opt" else "ocamlopt"
-
-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;
-  print "# "; print s; print " #\n";
-  print sep2;
-  print sep;
-  print "\n"
-
-let usage () =
-  output_string stderr "Usage summary:
-
-coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
-  command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath]
-  ... [VARIABLE = value] ...  [-opt|-byte] [-impredicative-set] [-no-install]
-  [-f file] [-o file] [-h] [--help]
-
-[file.v]: Coq file to be compiled
-[file.ml]: Objective Caml file to be compiled
-[subdirectory] : subdirectory that should be \"made\"
-[-custom command dependencies file]: add target \"file\" with command
-  \"command\" and dependencies \"dependencies\"
-[-I dir]: look for dependencies in \"dir\"
-[-R physicalpath logicalpath]: look for dependencies resursively 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
-[-impredicative-set]: compile with option -impredicative-set of coq
-[-no-install]: build a makefile with no install target
-[-f file]: take the contents of file as arguments
-[-o file]: output should go in file file
-[-h]: print this usage summary
-[--help]: equivalent to [-h]\n";
-  exit 1
-
-let is_genrule r =
-    let genrule = Str.regexp("%") in
-      Str.string_match genrule r 0
-
-let absolute_dir dir =
-  let current = Sys.getcwd () in
-    Sys.chdir dir;
-    let dir' = Sys.getcwd () in
-      Sys.chdir current;
-      dir'
-
-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] = '/')
-
-let canonize f =
-  let l = String.length f in
-  if l > 2 && f.[0] = '.' && f.[1] = '/' then
-    let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in
-    String.sub f n (l-n)
-  else f
-
-let is_absolute_prefix dir dir' =
-  is_prefix (absolute_dir dir) (absolute_dir dir')
-
-let is_included dir = function
-  | RInclude (dir',_) -> is_absolute_prefix dir' dir
-  | Include dir' -> absolute_dir dir = absolute_dir dir'
-  | _ -> false
-
-let has_top_file = function
-  | ML s | V s -> s = Filename.basename s
-  | _ -> false
-
-let physical_dir_of_logical_dir ldir =
-  let pdir = String.copy ldir in
-  for i = 0 to String.length ldir - 1 do
-    if pdir.[i] = '.' then pdir.[i] <- '/';
-  done;
-  pdir
-
-let standard ()=
-  print "byte:\n";
-  print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
-  print "opt:\n";
-  if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n";
-  print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n"
-
-let is_prefix_of_file dir f =
-  is_prefix dir (absolute_dir (Filename.dirname f))
-
-let classify_files_by_root var files (inc_i,inc_r) =
-  if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then
-    begin
-      (* Files in the scope of a -R option (assuming they are disjoint) *)
-      list_iter_i (fun i (pdir,ldir,abspdir) ->
-	if List.exists (is_prefix_of_file abspdir) files then
-	  printf "%s%d:=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
-	    var i pdir pdir var)
-	inc_r;
-      (* Files not in the scope of a -R option *)
-      let pat_of_dir (pdir,_,_) = pdir^"/%" in
-      let pdir_patterns = String.concat " " (List.map pat_of_dir inc_r) in
-      printf "%s0:=$(filter-out %s,$(%s))\n" var pdir_patterns var
-    end
-
-let install_include_by_root var files (_,inc_r) =
-  try
-    (* All files caught by a -R . option (assuming it is the only one) *)
-    let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in
-    let pdir = physical_dir_of_logical_dir ldir in
-    printf "\t(for i in $(%s); do \\\n" var;
-    printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir pdir;
-    printf "\t done)\n"
-  with Not_found ->
-    (* Files in the scope of a -R option (assuming they are disjoint) *)
-    list_iter_i (fun i (pdir,ldir,abspdir) ->
-      if List.exists (is_prefix_of_file abspdir) files then
-	begin
-	  let pdir' = physical_dir_of_logical_dir ldir in
-	  printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i;
-	  printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir' pdir';
-	  printf "\t done)\n"
-	end) inc_r;
-    (* Files not in the scope of a -R option *)
-    printf "\t(for i in $(%s0); do \\\n" var;
-    printf "\t install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
-    printf "\t done)\n"
-
-let install (vfiles,mlfiles,_,sds) inc =
-  print "install:\n";
-  print "\tmkdir -p $(COQLIB)/user-contrib\n";
-  if !some_vfile then install_include_by_root "VOFILES" vfiles inc;
-  if !some_mlfile then install_include_by_root "CMOFILES" mlfiles inc;
-  if !some_mlfile then install_include_by_root "CMIFILES" mlfiles inc;
-  if Coq_config.has_natdynlink && !some_mlfile then
-    install_include_by_root "CMXSFILES" mlfiles inc;
-  List.iter
-    (fun x ->
-      printf "\t(cd %s; $(MAKE) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x)
-    sds;
-  print "\n"
-
-let make_makefile sds =
-  if !make_name <> "" then begin
-    printf "%s: %s\n" !makefile_name !make_name;
-    printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name;
-    printf "\t$(COQBIN)coq_makefile -f %s -o %s\n" !make_name !makefile_name;
-    print "\n";
-    List.iter
-      (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n")
-      sds;
-    print "\n";
-  end
-
-let clean sds sps =
-  print "clean:\n";
-  print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
-  print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
-         $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
-  if !some_mlfile then
-    print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n";
-  print "\t- rm -rf html\n";
-  List.iter
-    (fun (file,_,_) ->
-       if not (is_genrule file) then
-	 (print "\t- rm -f "; print file; print "\n"))
-    sps;
-  List.iter
-    (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")
-    sds;
-  print "\n\n";
-  print "printenv: \n\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n";
-  print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n"
-
-let header_includes () = ()
-
-let footer_includes () =
-  if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
-  if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n"
-
-let implicit () =
-  let ml_rules () =
-    print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
-    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
-    print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
-    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 "%.cmxs: %.ml4\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
-    print "%.ml.d: %.ml\n";
-    print "\t$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $(PP) \"$<\" > \"$@\"\n\n"
-  and v_rule () =
-    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) -latex $< -o $@\n\n";
-    print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n";
-    print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n";
-    print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n";
-    print "%.v.d: %.v\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-  in
-    if !some_mlfile then ml_rules ();
-    if !some_vfile then v_rule ()
-
-let variables defs =
-  let var_aux (v,def) = print v; print "="; print def; print "\n" in
-    section "Variables definitions.";
-    print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n";
-    if !opt = "-byte" then
-      print "override OPT:=-byte\n"
-    else
-      print "OPT:=\n";
-    if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
-    (* Coq executables and relative variables *)
-    print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
-    print "ifdef CAMLBIN\n  COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)\nendif\n";
-    print "COQC:=$(COQBIN)coqc\n";
-    print "COQDEP:=$(COQBIN)coqdep -c\n";
-    print "GALLINA:=$(COQBIN)gallina\n";
-    print "COQDOC:=$(COQBIN)coqdoc\n";
-    print "COQMKTOP:=$(COQBIN)coqmktop\n";
-    (* Caml executables and relative variables *)
-    printf "CAMLLIB:=$(shell $(CAMLBIN)%s -where)\n" best_ocamlc;
-    printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc;
-    printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt;
-    printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
-    printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
-    print "GRAMMARS:=grammar.cma\n";
-    print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
-    print "CAMLP4OPTIONS:=\n";
-    List.iter var_aux defs;
-    print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n";
-    print "\n"
-
-let parameters () =
-  print "# \n";
-  print "# This Makefile may take 3 arguments passed as environment variables:\n";
-  print "#   - COQBIN to specify the directory where Coq binaries resides;\n";
-  print "#   - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n";
-  print "COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\\\/\\\\\\\\/g')\n";
-  print "CAMLP4:=\"$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\"\n";
-  print "ifndef CAMLP4BIN\n  CAMLP4BIN:=$(CAMLBIN)\nendif\n\n";
-  print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\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_absolute_prefix i' i) inc_r)) inc_i 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.";
-    print "OCAMLLIBS:="; print_list "\\\n  " str_i; print "\n";
-    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";
-    List.iter (fun c -> print " \\
-  -I $(COQLIB)/plugins/"; print c) Coq_config.plugins_dirs; print "\n";
-    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"
-
-
-let rec special = function
-  | [] -> []
-  | Special (file,deps,com) :: r -> (file,deps,com) :: (special r)
-  | _ :: r -> special r
-
-let custom sps =
-  let pr_path (file,dependencies,com) =
-    print file; print ": "; print dependencies; print "\n";
-    if com <> "" then (print "\t"; print com); print "\n\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"
-  in
-    if sds <> [] then section "Subdirectories.";
-    List.iter pr_subdir sds;
-    section "Special targets.";
-    print ".PHONY: ";
-    print_list " "
-      ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install"
-	:: "depend" :: "html" :: sds);
-    print "\n\n"
-
-let rec split_arguments = function
-  | V n :: r ->
-      let (v,m,o,s),i,d = split_arguments r in ((canonize n::v,m,o,s),i,d)
-  | ML n :: r ->
-      let (v,m,o,s),i,d = split_arguments r in ((v,canonize n::m,o,s),i,d)
-  | Special (n,dep,c) :: r ->
-      let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d)
-  | Subdir n :: r ->
-      let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d)
-  | Include p :: r ->
-      let t,(i,r),d = split_arguments r in (t,((p,absolute_dir p)::i,r),d)
-  | RInclude (p,l) :: r ->
-      let t,(i,r),d = split_arguments r in (t,(i,(p,l,absolute_dir p)::r),d)
-  | Def (v,def) :: r ->
-      let t,i,d = split_arguments r in (t,i,(v,def)::d)
-  | [] -> ([],[],[],[]),([],[]),[]
-
-let main_targets vfiles mlfiles other_targets inc =
-    if !some_vfile then
-      begin
-	print "VFILES:="; print_list "\\\n  " vfiles; print "\n";
-	print "VOFILES:=$(VFILES:.v=.vo)\n";
-	classify_files_by_root "VOFILES" vfiles 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"
-      end;
-    if !some_mlfile then
-      begin
-	print "MLFILES:="; print_list "\\\n  " mlfiles; print "\n";
-	print "CMOFILES:=$(MLFILES:.ml=.cmo)\n";
-	classify_files_by_root "CMOFILES" mlfiles inc;
-	print "CMIFILES:=$(MLFILES:.ml=.cmi)\n";
-	classify_files_by_root "CMIFILES" mlfiles inc;
-	print "CMXFILES:=$(MLFILES:.ml=.cmx)\n";
-	print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n";
-	classify_files_by_root "CMXSFILES" mlfiles inc;
-	print "OFILES:=$(MLFILES:.ml=.o)\n";
-      end;
-    print "\nall: ";
-    if !some_vfile then print "$(VOFILES) ";
-    if !some_mlfile then print "$(CMOFILES) ";
-    if Coq_config.has_natdynlink && !some_mlfile then print "$(CMXSFILES) ";
-    print_list "\\\n  " other_targets; print "\n";
-    if !some_vfile then
-      begin
-	print "spec: $(VIFILES)\n\n";
-	print "gallina: $(GFILES)\n\n";
-	print "html: $(GLOBFILES) $(VFILES)\n";
-	print "\t- mkdir -p html\n";
-	print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
-	print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
-	print "\t- mkdir -p html\n";
-	print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
-	print "all.ps: $(VFILES)\n";
-	print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
-	print "all-gal.ps: $(VFILES)\n";
-	print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
-	print "all.pdf: $(VFILES)\n";
-	print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
-	print "all-gal.pdf: $(VFILES)\n";
-	print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
-	print "\n\n"
-      end
-
-let all_target (vfiles, mlfiles, sps, sds) inc =
-  let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in
-  let other_targets = List.map (fun x,_,_ -> x) special_targets @ sds in
-  section "Definition of the \"all\" target.";
-  main_targets vfiles mlfiles other_targets inc;
-  custom sps;
-  subdirs sds
-
-let parse f =
-  let rec string = parser
-    | [< '' ' | '\n' | '\t' >] -> ""
-    | [< 'c; s >] -> (String.make 1 c)^(string s)
-    | [< >] -> ""
-  and string2 = parser
-    | [< ''"' >] -> ""
-    | [< 'c; s >] -> (String.make 1 c)^(string2 s)
-  and skip_comment = parser
-    | [< ''\n'; s >] -> s
-    | [< 'c; s >] -> skip_comment s
-    | [< >] -> [< >]
-  and args = parser
-    | [< '' ' | '\n' | '\t'; s >] -> args s
-    | [< ''#'; s >] -> args (skip_comment s)
-    | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s
-    | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s)
-    | [< >] -> []
-  in
-  let c = open_in f in
-  let res = args (Stream.of_channel c) in
-    close_in c;
-    res
-
-let rec process_cmd_line = function
-  | [] ->
-      some_file := !some_file or !some_mlfile or !some_vfile; []
-  | ("-h"|"--help") :: _ ->
-      usage ()
-  | ("-no-opt"|"-byte") :: r ->
-      opt := "-byte"; process_cmd_line r
-  | ("-full"|"-opt") :: r ->
-      opt := "-opt"; process_cmd_line r
-  | "-impredicative-set" :: r ->
-      impredicative_set := true; process_cmd_line r
-  | "-no-install" :: r ->
-      no_install := true; process_cmd_line r
-  | "-custom" :: com :: dependencies :: file :: r ->
-      let check_dep f =
-	if Filename.check_suffix f ".v" then
-          some_vfile := true
-	else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then
-          some_mlfile := true
-      in
-	List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies);
-	Special (file,dependencies,com) :: (process_cmd_line r)
-  | "-I" :: d :: r ->
-      Include d :: (process_cmd_line r)
-  | "-R" :: p :: l :: r ->
-      RInclude (p,l) :: (process_cmd_line r)
-  | ("-I"|"-custom") :: _ ->
-      usage ()
-  | "-f" :: file :: r ->
-      make_name := file;
-      process_cmd_line ((parse file)@r)
-  | ["-f"] ->
-      usage ()
-  | "-o" :: file :: r ->
-      makefile_name := file;
-      output_channel := (open_out file);
-      (process_cmd_line r)
-  | v :: "=" :: def :: r ->
-      Def (v,def) :: (process_cmd_line r)
-  | f :: r ->
-      if Filename.check_suffix f ".v" then begin
-          some_vfile := true;
-	  V f :: (process_cmd_line r)
-	end else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then begin
-          some_mlfile := true;
-	  ML f :: (process_cmd_line r)
-	end else if (Filename.check_suffix f ".mli") then begin
-	  Printf.eprintf "Warning: no need for .mli files, skipped %s\n" f;
-	  process_cmd_line r
-	end else
-          Subdir f :: (process_cmd_line r)
-
-let banner () =
-  print (Printf.sprintf
-"#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \\VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V%s ##
-#############################################################################
-
-" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
-
-let warning () =
-  print "# WARNING\n#\n";
-  print "# This Makefile has been automagically generated\n";
-  print "# Edit at your own risks !\n";
-  print "#\n# END OF WARNING\n\n"
-
-let print_list l = List.iter (fun x -> print x; print " ") l
-
-let command_line args =
-  print "#\n# This Makefile was generated by the command line :\n";
-  print "# coq_makefile ";
-  print_list args;
-  print "\n#\n\n"
-
-let directories_deps l =
-  let print_dep f dep =
-    if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end
-  in
-  let rec iter ((dirs,before) as acc) = function
-    | [] ->
-	()
-    | (Subdir d) :: l ->
-	print_dep d before; iter (d :: dirs, d :: before) l
-    | (ML f) :: l ->
-	print_dep f dirs; iter (dirs, f :: before) l
-    | (V f) :: l ->
-	print_dep f dirs; iter (dirs, f :: before) l
-    | (Special (f,_,_)) :: l ->
-	print_dep f dirs; iter (dirs, f :: before) l
-    | _ :: l ->
-	iter acc l
-  in
-    iter ([],[]) l
-
-let ensure_root_dir l =
-  if List.exists (is_included ".") l or not (List.exists has_top_file l) then
-    l
-  else
-    Include "." :: l
-
-let warn_install_at_root_directory (vfiles,mlfiles,_,_) (inc_i,inc_r) =
-  let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in
-  let inc_top = List.map (fun (p,_,a) -> (p,a)) inc_r_top @ inc_i in
-  let files = vfiles @ mlfiles in
-  if not !no_install &&
-    List.exists (fun f -> List.mem_assoc (Filename.dirname f) inc_top) 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 ")
-
-let check_overlapping_include (inc_i,inc_r) =
-  let pwd = Sys.getcwd () in
-  let rec 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
-	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
-	List.iter (fun (pdir',abspdir') ->
-	  if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then
-	    Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i
-  in aux inc_r
-
-let do_makefile args =
-  let l = process_cmd_line args in
-  let l = ensure_root_dir l in
-  let (_,_,sps,sds as targets), inc, defs = split_arguments l in
-  warn_install_at_root_directory targets inc;
-  check_overlapping_include inc;
-  banner ();
-  header_includes ();
-  warning ();
-  command_line args;
-  parameters ();
-  include_dirs inc;
-  variables defs;
-  all_target targets inc;
-  implicit ();
-  standard ();
-  if not !no_install then install targets inc;
-  clean sds sps;
-  make_makefile sds;
-  (* TEST directories_deps l; *)
-  footer_includes ();
-  warning ();
-  if not (!output_channel == stdout) then close_out !output_channel;
-  exit 0
-
-let main () =
-  let args =
-    if Array.length Sys.argv = 1 then usage ();
-    List.tl (Array.to_list Sys.argv)
-  in
-    do_makefile args
-
-let _ = Printexc.catch main ()
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml
index 14a37a2e..350b59aa 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_tex.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* coq-tex
  * JCF, 16/1/98
  * adapted from caml-tex (perl script written by Xavier Leroy)
@@ -15,15 +13,6 @@
  * Perl isn't as portable as it pretends to be, and is quite difficult
  * to read and maintain... Let us rewrite the stuff in Caml! *)
 
-let _ =
-  match Sys.os_type with
-    | "Unix" -> ()
-    | _ -> begin
-      	print_string "This program only runs under Unix !\n";
-      	flush stdout;
-      	exit 1
-      end
-
 let linelen = ref 72
 let output = ref ""
 let output_specified = ref false
@@ -33,6 +22,7 @@ let verbose = ref false
 let slanted = ref false
 let hrule = ref false
 let small = ref false
+let boot = ref false
 
 let coq_prompt = Str.regexp "Coq < "
 let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
@@ -88,21 +78,23 @@ let bang    = Str.regexp "!"
 let expos   = Str.regexp "^"
 
 let tex_escaped s =
-  let rec trans = parser
-    | [< s1 = (parser
-		 | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] ->
-		     "\\" ^ (String.make 1 c)
-		 | [< ''\\' >] -> "{\\char'134}"
-		 | [< ''^'  >] -> "{\\char'136}"
-		 | [< ''~'  >] -> "{\\char'176}"
-		 | [< '' '  >] -> "~"
-		 | [< ''<'  >] -> "{<}"
-		 | [< ''>'  >] -> "{>}"
-		 | [< 'c >]    -> String.make 1 c);
-	 s2 = trans >] -> s1 ^ s2
-    | [< >] -> ""
+  let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
+  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in
+  let adapt_delim = function
+    | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "\\" -> "{\\char'134}"
+    | "^" -> "{\\char'136}"
+    | "~" -> "{\\char'176}"
+    | " " -> "~"
+    | "<" -> "{<}"
+    | ">" -> "{>}"
+    | _ -> assert false
   in
-  trans (Stream.of_string s)
+  let adapt = function
+    | Str.Text s -> s
+    | Str.Delim s -> adapt_delim s
+  in
+  String.concat "" (List.map adapt (Str.full_split delims s))
 
 let encapsule sl c_out s =
   if sl then
@@ -198,11 +190,11 @@ let insert texfile coq_output result =
     else begin
       if !verbose then Printf.printf "Coq < %s\n" s;
       if has_match dot_end_line s then
-       	let bl = next_block (succ k) in
+	let bl = next_block (succ k) in
 	if !verbose then List.iter print_endline bl;
 	eval 0
       else
-       	eval (succ k)
+	eval (succ k)
     end
   in
   try
@@ -268,18 +260,29 @@ let parse_cl () =
 	"-hrule", Arg.Set hrule,
 	"           Coq parts are written between 2 horizontal lines";
 	"-small", Arg.Set small,
-	"           Coq parts are written in small font"
+	"           Coq parts are written in small font";
+	"-boot", Arg.Set boot,
+	"           Launch coqtop with the -boot option"
       ]
       (fun s -> files := s :: !files)
       "coq-tex [options] file ..."
 
+let find_coqtop () =
+  let prog = Sys.executable_name in
+  try
+    let size = String.length prog in
+    let i = Str.search_backward (Str.regexp_string "coq-tex") prog (size-7) in
+    (String.sub prog 0 i)^"coqtop"^(String.sub prog (i+7) (size-i-7))
+  with Not_found -> begin
+    Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
+    "coqtop"
+  end
+
 let main () =
   parse_cl ();
-  if !image = "" then begin
-    Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
-    image := "coqtop"
-  end;
-  if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin
+  if !image = "" then image := Filename.quote (find_coqtop ());
+  if !boot then image := !image ^ " -boot";
+  if Sys.command (!image ^ " -batch -silent") <> 0 then begin
     Printf.printf "Error: ";
     let _ = Sys.command (!image ^ " -batch") in
     exit 1
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index d36fdae3..90cdd12d 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Printf
 open Coqdep_lexer
 open Coqdep_common
@@ -40,7 +38,7 @@ let rec warning_mult suf iter =
 let add_coqlib_known phys_dir log_dir f =
   match get_extension f [".vo"] with
     | (basename,".vo") ->
-	let name = log_dir@[basename] in
+        let name = log_dir@[basename] in
 	let paths = suffixes name in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
@@ -192,6 +190,7 @@ let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   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
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "plugins" ["Coq"]
@@ -200,7 +199,9 @@ let coqdep () =
     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 []
+    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;
   end;
   List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
   List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 68197e0c..19aba41d 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep_boot.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Coqdep_common
 
 (** [coqdep_boot] is a stripped-down version of [coqdep], whose
@@ -22,6 +20,8 @@ let rec parse = function
   | "-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 *)
+  | "-mldep" :: ocamldep :: ll ->
+      option_mldep := Some ocamldep; option_c := true; parse ll
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 5d06b888..4977a94c 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep_common.ml 11984 2009-03-16 13:41:49Z letouzey $ *)
-
 open Printf
 open Coqdep_lexer
 open Unix
@@ -26,6 +24,7 @@ let option_c = ref false
 let option_noglob = ref false
 let option_slash = ref false
 let option_natdynlk = ref true
+let option_mldep = ref None
 
 let norecdir_list = ref ([]:string list)
 
@@ -63,6 +62,7 @@ let basename_noext filename =
 let mlAccu  = ref ([] : (string * string * dir) list)
 and mliAccu = ref ([] : (string * dir) list)
 and mllibAccu = ref ([] : (string * dir) list)
+and mlpackAccu = ref ([] : (string * dir) list)
 
 (** Coq files specifies on the command line:
     - first string is the full filename, with only its extension removed
@@ -108,12 +108,17 @@ let mkknown () =
 let add_ml_known, iter_ml_known, search_ml_known = mkknown ()
 let add_mli_known, iter_mli_known, search_mli_known = mkknown ()
 let add_mllib_known, _, search_mllib_known = mkknown ()
+let add_mlpack_known, _, search_mlpack_known = mkknown ()
 
 let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t)
 let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
 
 let clash_v = ref ([]: (string list * string list) list)
 
+let error_cannot_parse s (i,j) =
+  Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
+  exit 1
+
 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"
@@ -122,12 +127,12 @@ let warning_module_notfound f s =
 
 let warning_notfound f s =
   eprintf "*** Warning: in file %s, the file " f;
-  eprintf "%s.v is required and has not been found !\n" s;
+  eprintf "%s.v is required and has not been found!\n" s;
   flush stderr
 
 let warning_declare f s =
   eprintf "*** Warning: in file %s, declared ML module " f;
-  eprintf "%s has not been found !\n" s;
+  eprintf "%s has not been found!\n" s;
   flush stderr
 
 let warning_clash file dir =
@@ -178,7 +183,26 @@ let depend_ML str =
 	(" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
-let traite_fichier_ML md ext =
+let soustraite_fichier_ML dep md ext =
+  try
+    let chan = open_process_in (dep^" -modules "^md^ext) in
+    let list = ocamldep_parse (Lexing.from_channel chan) in
+    let a_faire = ref "" in
+    let a_faire_opt = ref "" in
+    List.iter
+      (fun str ->
+	 let byte,opt = depend_ML str in
+	 a_faire := !a_faire ^ byte;
+	 a_faire_opt := !a_faire_opt ^ opt)
+      (List.rev list);
+    (!a_faire, !a_faire_opt)
+  with
+    | Sys_error _ -> ("","")
+    | _ ->
+       Printf.eprintf "Coqdep: subprocess %s failed on file %s%s\n" dep md ext;
+       exit 1
+
+let autotraite_fichier_ML md ext =
   try
     let chan = open_in (md ^ ext) in
     let buf = Lexing.from_channel chan in
@@ -203,22 +227,29 @@ let traite_fichier_ML md ext =
     (!a_faire, !a_faire_opt)
   with Sys_error _ -> ("","")
 
-let traite_fichier_mllib md ext =
+let traite_fichier_ML md ext =
+  match !option_mldep with
+    | Some dep -> soustraite_fichier_ML dep md ext
+    | None -> autotraite_fichier_ML md ext
+
+let traite_fichier_modules md ext =
   try
     let chan = open_in (md ^ ext) in
     let list = mllib_list (Lexing.from_channel chan) in
-    let a_faire = ref "" in
-    let a_faire_opt = ref "" in
-    List.iter
-      (fun str -> match search_ml_known str with
-	 | Some mldir ->
-	     let file = file_name str mldir in
-	     a_faire := !a_faire^" "^file^".cmo";
-	     a_faire_opt := !a_faire_opt^" "^file^".cmx"
-	 | None -> ()) list;
-    (!a_faire, !a_faire_opt)
-  with Sys_error _ -> ("","")
-
+    List.fold_left
+      (fun a_faire str -> match search_mlpack_known str with
+	| Some mldir ->
+	  let file = file_name str mldir in
+	  a_faire^" "^file
+	| None ->
+	  match search_ml_known str with
+	    | Some mldir ->
+	      let file = file_name str mldir in
+	      a_faire^" "^file
+	    | None -> a_faire) "" list
+  with
+    | Sys_error _ -> ""
+    | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
 
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
    other special characters are escaped by backslash prefixing while
@@ -257,7 +288,7 @@ let canonize f =
     | (f,_) :: _ -> escape f
     | _ -> escape f
 
-let traite_fichier_Coq verbose f =
+let rec traite_fichier_Coq verbose f =
   try
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
@@ -302,9 +333,12 @@ let traite_fichier_Coq verbose f =
 		  match search_mllib_known s with
 		    | Some mldir -> declare ".cma" mldir s
 		    | None ->
-			match search_ml_known s with
-			  | Some mldir -> declare ".cmo" mldir s
-			  | None -> warning_declare f str
+		      match search_mlpack_known s with
+			| Some mldir -> declare ".cmo" mldir s
+			| None ->
+			  match search_ml_known s with
+			    | Some mldir -> declare ".cmo" mldir s
+			    | None -> warning_declare f str
 		end
 	      in List.iter decl sl
 	  | Load str ->
@@ -313,12 +347,15 @@ let traite_fichier_Coq verbose f =
 	        addQueue deja_vu_v [str];
                 try
                   let file_str = Hashtbl.find vKnown [str] in
-                  printf " %s.v" (canonize file_str)
+                  let canon = canonize file_str in
+                  printf " %s.v" canon;
+                  traite_fichier_Coq true (canon ^ ".v")
                 with Not_found -> ()
        	      end
+          | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
       done
-    with Fin_fichier -> ();
-      close_in chan
+    with Fin_fichier -> close_in chan
+       | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j)
   with Sys_error _ -> ()
 
 
@@ -346,19 +383,30 @@ let mL_dependencies () =
   List.iter
     (fun (name,dirname) ->
        let fullname = file_name name dirname in
-       let (dep,dep_opt) = traite_fichier_mllib fullname ".mllib" in
+       let dep = traite_fichier_modules fullname ".mllib" in
+       let efullname = escape fullname in
+       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
+       printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname;
+       flush stdout)
+    (List.rev !mllibAccu);
+  List.iter
+    (fun (name,dirname) ->
+       let fullname = file_name name dirname in
+       let dep = traite_fichier_modules fullname ".mlpack" in
        let efullname = escape fullname in
-       printf "%s.cma:%s\n" efullname dep;
-       printf "%s.cmxa %s.cmxs:%s\n" efullname efullname dep_opt;
+       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
+       printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname efullname;
        flush stdout)
-    (List.rev !mllibAccu)
+    (List.rev !mlpackAccu)
 
 let coq_dependencies () =
   List.iter
     (fun (name,_) ->
        let ename = escape name in
        let glob = if !option_noglob then "" else " "^ename^".glob" in
-       printf "%s%s%s: %s.v" ename !suffixe glob ename;
+       printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
        traite_fichier_Coq true (name ^ ".v");
        printf "\n";
        flush stdout)
@@ -370,7 +418,7 @@ let rec suffixes = function
   | dir::suffix as l -> l::suffixes suffix
 
 let add_known phys_dir log_dir f =
-  match get_extension f [".v";".ml";".mli";".ml4";".mllib"] with
+  match get_extension f [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
@@ -380,6 +428,7 @@ let add_known phys_dir log_dir f =
     | (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)
     | _ -> ()
 
 (* Visits all the directories under [dir], including [dir],
@@ -432,7 +481,7 @@ let rec treat_file old_dirname old_name =
 	     while true do treat_file (Some newdirname) (readdir dir) done
 	   with End_of_file -> closedir dir)
     | S_REG ->
-	(match get_extension name [".v";".ml";".mli";".ml4";".mllib"] with
+	(match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
 	   | (base,".v") ->
 	       let name = file_name base dirname
 	       and absname = absolute_file_name base dirname in
@@ -440,5 +489,6 @@ let rec treat_file old_dirname old_name =
 	   | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname)
 	   | (base,".mli") -> addQueue mliAccu (base,dirname)
 	   | (base,".mllib") -> addQueue mllibAccu (base,dirname)
+	   | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
 	   | _ -> ())
     | _ -> ()
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
new file mode 100644
index 00000000..afc171cb
--- /dev/null
+++ b/tools/coqdep_common.mli
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val option_c : bool ref
+val option_noglob : bool ref
+val option_slash : bool ref
+val option_natdynlk : bool ref
+val option_mldep : string option ref
+val norecdir_list : string list ref
+val suffixe : string ref
+type dir = string option
+val ( // ) : string -> string -> string
+val get_extension : string -> string list -> string * string
+val basename_noext : string -> string
+val mlAccu : (string * string * dir) list ref
+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 iter_ml_known : (string -> dir -> unit) -> unit
+val search_ml_known : string -> dir option
+val add_mli_known : string -> dir -> unit
+val iter_mli_known : (string -> dir -> unit) -> unit
+val search_mli_known : string -> dir option
+val add_mllib_known : string -> dir -> unit
+val search_mllib_known : string -> dir option
+val vKnown : (string list, string) Hashtbl.t
+val coqlibKnown : (string list, unit) Hashtbl.t
+val file_name : string -> string option -> string
+val escape : string -> string
+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_directory :
+  bool ->
+  (string -> string list -> string -> unit) -> string -> string list -> unit
+val add_dir :
+  (string -> string list -> string -> unit) -> string -> string list -> unit
+val add_rec_dir :
+  (string -> string list -> string -> unit) -> string -> string list -> unit
+val treat_file : dir -> string -> unit
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
new file mode 100644
index 00000000..7cea9743
--- /dev/null
+++ b/tools/coqdep_lexer.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type mL_token = Use_module of string
+
+type qualid = string list
+
+type coq_token =
+    Require of qualid list
+  | RequireString of string
+  | Declare of string list
+  | Load of string
+  | AddLoadPath of string
+  | AddRecLoadPath of string * qualid
+
+exception Fin_fichier
+exception Syntax_error of int * int
+
+val coq_action : Lexing.lexbuf -> coq_token
+val caml_action : Lexing.lexbuf -> mL_token
+val mllib_list : Lexing.lexbuf -> string list
+val ocamldep_parse : Lexing.lexbuf -> string list
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 28ea4200..f59d6a0f 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqdep_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 {
 
   open Filename
@@ -15,26 +13,42 @@
 
   type mL_token = Use_module of string
 
-  type spec = bool
+  type qualid = string list
 
   type coq_token =
-    | Require of string list list
+    | Require of qualid list
     | RequireString of string
-    | Declare of string list
+    | Declare of string list (* Names are assumed to be uncapitalized *)
     | Load of string
+    | AddLoadPath of string
+    | AddRecLoadPath of string * qualid
 
   let comment_depth = ref 0
 
   exception Fin_fichier
+  exception Syntax_error of int*int
 
   let module_current_name = ref []
   let module_names = ref []
   let ml_module_name = ref ""
+  let loadpath = ref ""
 
   let mllist = ref ([] : string list)
 
   let field_name s = String.sub s 1 (String.length s - 1)
 
+  let unquote_string s =
+    String.sub s 1 (String.length s - 2)
+
+  let unquote_vfile_string s =
+    let f = unquote_string s in
+    if check_suffix f ".v" then chop_suffix f ".v" else f
+
+  let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
+    lexbuf.lex_curr_p <- lexbuf.lex_start_p
+
+  let syntax_error lexbuf =
+    raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
 }
 
 let space = [' ' '\t' '\n' '\r']
@@ -42,31 +56,71 @@ let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
 let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
 let identchar =
   ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
-let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+
-let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+
 let caml_up_ident = uppercase identchar*
 let caml_low_ident = lowercase identchar*
+
+let coq_firstchar =
+  (* This is only an approximation, refer to lib/util.ml for correct def *)
+  ['A'-'Z' 'a'-'z' '_'] |
+  (* superscript 1 *)
+  '\194' '\185' |
+  (* utf-8 latin 1 supplement *)
+  '\195' ['\128'-'\150'] | '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] |
+  (* utf-8 letters *)
+  '\206' (['\145'-'\161'] | ['\163'-'\187'])
+  '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+    | '\129' [ '\176'-'\187' ] (* superscripts *)
+    | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+let coq_identchar = coq_firstchar | ['\'' '0'-'9']
+let coq_ident = coq_firstchar coq_identchar*
+let coq_field = '.' coq_ident
+
 let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
   | "Require" space+
-      { module_names := []; opened_file lexbuf }
+      { require_file lexbuf }
   | "Require" space+ "Export" space+
-      { module_names := []; opened_file lexbuf}
+      { require_file lexbuf}
   | "Require" space+ "Import" space+
-      { module_names := []; opened_file lexbuf}
+      { require_file lexbuf}
   | "Local"? "Declare" space+ "ML" space+ "Module" space+
       { mllist := []; modules lexbuf}
   | "Load" space+
       { load_file lexbuf }
-  | "\""
-      { string lexbuf; coq_action lexbuf}
-  | "(*" (* "*)" *)
+  | "Add" space+ "LoadPath" space+
+      { add_loadpath lexbuf }
+  | space+
+      { coq_action lexbuf }
+  | "(*"
       { comment_depth := 1; comment lexbuf; coq_action lexbuf }
   | eof
       { raise Fin_fichier}
   | _
-      { coq_action lexbuf }
+      { skip_to_dot lexbuf; coq_action lexbuf }
+
+and add_loadpath = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; add_loadpath lexbuf }
+  | space+
+      { add_loadpath lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | '"' [^ '"']* '"' (*'"'*)
+      { loadpath := unquote_string (lexeme lexbuf);
+        add_loadpath_as lexbuf }
+
+and add_loadpath_as = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; add_loadpath_as lexbuf }
+  | space+
+      { add_loadpath_as lexbuf }
+  | "as"
+      { let qid = coq_qual_id lexbuf in
+        skip_to_dot lexbuf;
+        AddRecLoadPath (!loadpath,qid) }
+  | dot
+      { AddLoadPath !loadpath }
 
 and caml_action = parse
   | space +
@@ -133,7 +187,8 @@ and comment = parse
       { comment lexbuf }
   | eof
       { raise Fin_fichier }
-  | _ { comment lexbuf }
+  | _
+      { comment lexbuf }
 
 and string = parse
   | '"' (* '"' *)
@@ -152,69 +207,108 @@ and string = parse
 and load_file = parse
   | '"' [^ '"']* '"' (*'"'*)
       { let s = lexeme lexbuf in
-	let f = String.sub s 1 (String.length s - 2) in
-	skip_to_dot lexbuf;
-	Load (if check_suffix f ".v" then chop_suffix f ".v" else f) }
+	parse_dot lexbuf;
+	Load (unquote_vfile_string s) }
   | coq_ident
       { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
   | eof
-      { raise Fin_fichier }
+      { syntax_error lexbuf }
   | _
-      { load_file lexbuf }
+      { syntax_error lexbuf }
+
+and require_file = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; require_file lexbuf }
+  | space+
+      { require_file lexbuf }
+  | coq_ident
+      { module_current_name := [Lexing.lexeme lexbuf];
+        module_names := [coq_qual_id_tail lexbuf];
+        let qid = coq_qual_id_list lexbuf in
+        parse_dot lexbuf;
+        Require qid }
+  | '"' [^'"']* '"' (*'"'*)
+      { let s = Lexing.lexeme lexbuf in
+        parse_dot lexbuf;
+        RequireString (unquote_vfile_string s) }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { syntax_error lexbuf }
 
 and skip_to_dot = parse
   | dot { () }
-  | eof { () }
+  | eof { syntax_error lexbuf }
   | _   { skip_to_dot lexbuf }
 
-and opened_file = parse
-  | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file lexbuf }
+and parse_dot = parse
+  | dot { () }
+  | eof { syntax_error lexbuf }
+  | _ { syntax_error lexbuf }
+
+and coq_qual_id = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; coq_qual_id lexbuf }
   | space+
-      	       	{ opened_file lexbuf }
+      { coq_qual_id lexbuf }
   | coq_ident
-       	       	{ module_current_name := [Lexing.lexeme lexbuf];
-                  opened_file_fields lexbuf }
-
-  | '"' [^'"']* '"'   { (*'"'*)
-                        let lex = Lexing.lexeme lexbuf in
-      	       	       	let str = String.sub lex 1 (String.length lex - 2) in
-                        let str =
-                          if Filename.check_suffix str ".v" then
-                            Filename.chop_suffix str ".v"
-                          else str in
-			RequireString str }
-  | eof         { raise Fin_fichier }
-  | _           { opened_file lexbuf }
-
-and opened_file_fields = parse
-  | "(*" (* "*)" *)
-                { comment_depth := 1; comment lexbuf;
-                  opened_file_fields lexbuf }
+      { module_current_name := [Lexing.lexeme lexbuf];
+        coq_qual_id_tail lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { backtrack lexbuf;
+        let qid = List.rev !module_current_name in
+        module_current_name := [];
+        qid }
+
+and coq_qual_id_tail = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; coq_qual_id_tail lexbuf }
   | space+
-                { opened_file_fields lexbuf }
+      { coq_qual_id_tail lexbuf }
   | coq_field
-                { module_current_name :=
-                    field_name (Lexing.lexeme lexbuf) :: !module_current_name;
-                  opened_file_fields lexbuf }
-  | coq_ident   { module_names :=
-                    List.rev !module_current_name :: !module_names;
-                  module_current_name := [Lexing.lexeme lexbuf];
-                  opened_file_fields lexbuf }
-  | dot         { module_names :=
-                    List.rev !module_current_name :: !module_names;
-                  Require (List.rev !module_names) }
-  | eof         { raise Fin_fichier }
-  | _           { opened_file_fields lexbuf }
+      { module_current_name :=
+          field_name (Lexing.lexeme lexbuf) :: !module_current_name;
+        coq_qual_id_tail lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { backtrack lexbuf;
+        let qid = List.rev !module_current_name in
+        module_current_name := [];
+        qid }
+
+and coq_qual_id_list = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; coq_qual_id_list lexbuf }
+  | space+
+      { coq_qual_id_list lexbuf }
+  | coq_ident
+      { module_current_name := [Lexing.lexeme lexbuf];
+        module_names := coq_qual_id_tail lexbuf :: !module_names;
+        coq_qual_id_list lexbuf
+      }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { backtrack lexbuf;
+        List.rev !module_names }
 
 and modules = parse
-  | space+              { modules lexbuf }
-  | "(*" (* "*)" *)	{ comment_depth := 1; comment lexbuf;
-      	       	       	  modules lexbuf }
+  | space+
+      { modules lexbuf }
+  | "(*"
+      { comment_depth := 1; comment lexbuf;
+        modules lexbuf }
   | '"' [^'"']* '"'
-        { let lex = (Lexing.lexeme lexbuf) in
-	  let str = String.sub lex 1 (String.length lex - 2) in
-	    mllist := str :: !mllist; modules lexbuf}
-  | _   { (Declare (List.rev !mllist)) }
+      { let lex = (Lexing.lexeme lexbuf) in
+	let str = String.sub lex 1 (String.length lex - 2) in
+	mllist := str :: !mllist; modules lexbuf}
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { (Declare (List.rev !mllist)) }
 
 and qual_id = parse
   | '.' [^ '.' '(' '['] {
@@ -223,10 +317,12 @@ and qual_id = parse
   | _ { caml_action lexbuf }
 
 and mllib_list = parse
-  | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
+  | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }
+  | "*predef*" { mllib_list lexbuf }
   | space+ { mllib_list lexbuf }
   | eof { [] }
+  | _ { syntax_error lexbuf }
 
-
-
+and ocamldep_parse = parse
+  | [^ ':' ]* ':' { mllib_list lexbuf }
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 83bfa5ed..8802c0ef 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 
 let norm_char_latin1 c = match Char.uppercase c with
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index ec5b084f..792b71fc 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* Alphabetic order. *)
 
 val compare_char : char -> char -> int
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5cb670dc..f37db46b 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-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -49,21 +49,40 @@ type glob_source_t =
 
 let glob_source = ref DotGlob
 
+(*s Manipulations of paths and path aliases *)
+
+let normalize_path p =
+  (* We use the Unix subsystem to normalize a physical path (relative
+     or absolute) and get rid of symbolic links, relative links (like
+     ./ or ../ in the middle of the path; it's tricky but it
+     works... *)
+  (* Rq: Sys.getcwd () returns paths without '/' at the end *)
+  let orig = Sys.getcwd () in
+  Sys.chdir p;
+  let res = Sys.getcwd () in
+  Sys.chdir orig;
+  res
+
+let normalize_filename f =
+  let basename = Filename.basename f in
+  let dirname = Filename.dirname f in
+  normalize_path dirname, basename
+
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
   let file = "states/initial.coq" in
-  if Sys.file_exists (Filename.concat Coq_config.coqlib file)
-  then Coq_config.coqlib
-  else
-    let coqbin = 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
-    else
-      Coq_config.coqlib
+  match Coq_config.coqlib with
+    | Some coqlib when Sys.file_exists (Filename.concat 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
+      else prefix
 
 let header_trailer = ref true
 let header_file = ref ""
@@ -90,6 +109,7 @@ let toc_depth = (ref None : int option ref)
 let lib_name = ref "Library"
 let lib_subtitles = ref false
 let interpolate = ref false
+let inline_notmono = ref false
 
 let charset = ref "iso-8859-1"
 let inputenc = ref ""
@@ -103,7 +123,7 @@ let set_latin1 () =
 
 let set_utf8 () =
   charset := "utf-8";
-  inputenc := "utf8";
+  inputenc := "utf8x";
   utf8 := true
 
 (* Parsing options *)
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 24b514b7..ccd285f1 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -101,8 +101,13 @@ h4.section {
     color: rgb(30%,30%,70%);
     font-family: monospace } 
 
-.doc .inlinecode .id {
-    color: rgb(30%,30%,70%);
+.doc .inlinecode .id { 
+    color: rgb(30%,30%,70%); 
+} 
+
+.inlinecodenm { 
+    display: inline;
+    color: #444444;
 }
 
 .doc .code { 
@@ -124,6 +129,32 @@ h4.section {
     font-family: monospace;
  } 
 
+table.infrule {
+  border: 0px;
+  margin-left: 50px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+td.infrule {
+    font-family: monospace;
+    text-align: center;
+/*    color: rgb(35%,35%,70%);  */
+    padding: 0px;
+    line-height: 100%;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%); 
+    font-size: 80%;
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
 /* Pied de page */
 
 #footer { font-size: 65%;
@@ -231,4 +262,13 @@ h4.section {
     position: absolute;
     bottom: 0;
     text-align: bottom;
-}
\ No newline at end of file
+}
+
+.paragraph {
+    height: 0.75em;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+}
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 085ae122..adc49ed4 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Index
 
 val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index a2bcb987..d7b54fd0 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*)
-
 (*s Utility functions for the scanners *)
 
 {
@@ -80,8 +77,17 @@
   let in_proof = ref None
   let in_emph = ref false
 
-  let start_emph () = in_emph := true; Output.start_emph ()
-  let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false)
+  let in_env start stop = 
+    let r = ref false in
+    let start_env () = r := true; start () in
+    let stop_env () = if !r then stop (); r := false in
+      (fun x -> !r), start_env, stop_env
+      
+  let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+  let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
+
+  let url_buffer = Buffer.create 40
+  let url_name_buffer = Buffer.create 40
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
     lexbuf.lex_curr_p <- lexbuf.lex_start_p
@@ -257,7 +263,7 @@
     let nbsp,isp = count_spaces s in
     Output.indentation nbsp;
     let s = String.sub s isp (String.length s - isp) in
-    Output.ident s (lexeme_start lexbuf + isp)
+    Output.keyword s (lexeme_start lexbuf + isp)
 
 }
 
@@ -323,6 +329,7 @@ let def_token =
   | "SubClass"
   | "Example"
   | "Fixpoint"
+  | "Function"
   | "Boxed"
   | "CoFixpoint"
   | "Record"
@@ -371,13 +378,17 @@ let commands =
   | "Drop"
   | "ProtectedLoop"
   | "Quit"
+  | "Restart"
   | "Load"
   | "Add"
   | "Remove" space+ "Loadpath"
   | "Print"
   | "Inspect"
   | "About"
+  | "SearchAbout"
+  | "SearchRewrite"
   | "Search"
+  | "Locate"
   | "Eval"
   | "Reset"
   | "Check"
@@ -405,6 +416,14 @@ let prog_kw =
   | "Obligations"
   | "Solve"
 
+let hint_kw = 
+  "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors"
+
+let set_kw =
+    "Printing" space+ ("Coercions" | "Universes" | "All")
+  | "Implicit" space+ "Arguments"
+  
+
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
   | "Ltac"
@@ -412,15 +431,16 @@ let gallina_kw_to_hide =
   | "Import"
   | "Export"
   | "Load"
-  | "Hint"
+  | "Hint" space+ hint_kw
   | "Open"
   | "Close"
   | "Delimit"
   | "Transparent"
   | "Opaque"
   | ("Declare" space+ ("Morphism" | "Step") )
-  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | ("Set" | "Unset") space+ set_kw
   | "Declare" space+ ("Left" | "Right") space+ "Step"
+  | "Debug" space+ ("On" | "Off")
 
 
 let section = "*" | "**" | "***" | "****"
@@ -512,7 +532,7 @@ rule coq_bol = parse
 	output_indented_keyword s lexbuf;
 	let eol= body lexbuf in
 	if eol then coq_bol lexbuf else coq lexbuf }
-  | space* notation_kw space*
+  | space* notation_kw
       {	let s = lexeme lexbuf in
 	output_indented_keyword s lexbuf;
 	let eol= start_notation_string lexbuf in
@@ -639,7 +659,7 @@ and coq = parse
 	  Output.ident s (lexeme_start lexbuf);
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
-  | notation_kw space*
+  | notation_kw
       { let s = lexeme lexbuf in
 	Output.ident s (lexeme_start lexbuf);
 	let eol= start_notation_string lexbuf in
@@ -663,8 +683,6 @@ and coq = parse
 (*s Scanning documentation, at beginning of line *)
 
 and doc_bol = parse
-  | space* nl+
-      { Output.paragraph (); doc_bol lexbuf }
   | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
       { let eol, lex = strip_eol (lexeme lexbuf) in
         let lev, s = sec_title lex in
@@ -674,33 +692,26 @@ and doc_bol = parse
           else
             Output.section lev (fun () -> ignore (doc None (from_string s)));
 	    if eol then doc_bol lexbuf else doc None lexbuf }
-  | space* nl space* '-'+
-      { (* adding this production instead of just letting the paragraph
-           production and the begin list production fire eliminates
-           extra vertical whitespace. *)
-        let buf' = lexeme lexbuf in
-        let buf =
-          let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
-            match bufs with
-              | (_ :: s :: []) -> s
-              | (_ :: _ :: s :: _) -> s
-              | _ -> eprintf "Internal error bad_split1 - please report\n";
-                     exit 1
+  | space_nl* '-'+
+      { let buf' = lexeme lexbuf in
+        let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
+        let lines = (List.length bufs) - 1 in
+        let line = 
+          match bufs with
+          | [] -> eprintf "Internal error bad_split1 - please report\n";
+                  exit 1
+          | _ -> List.nth bufs lines
         in
-          match check_start_list buf with
+          match check_start_list line with
           | Neither -> backtrack_past_newline lexbuf; doc None lexbuf
-          | List n -> Output.item 1; doc (Some [n]) lexbuf
-          | Rule -> Output.rule (); doc None lexbuf
-      }
-  | space* '-'+
-      { let buf = lexeme lexbuf in
-          match check_start_list buf with
-          | Neither -> backtrack lexbuf; doc None lexbuf
-          | List n -> Output.item 1; doc (Some [n]) lexbuf
+          | List n -> Output.paragraph ();
+                      Output.item 1; doc (Some [n]) lexbuf
           | Rule -> Output.rule (); doc None lexbuf
       }
+  | space* nl+
+      { Output.paragraph (); doc_bol lexbuf }
   | "<<" space*
-      { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
   | eof
       { true }
   | '_'
@@ -724,8 +735,8 @@ and doc_list_bol indents = parse
             backtrack lexbuf; doc_bol lexbuf
       }
   | "<<" space*
-      { Output.start_verbatim ();
-        verbatim lexbuf;
+      { Output.start_verbatim false;
+        verbatim false lexbuf;
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
@@ -734,6 +745,8 @@ and doc_list_bol indents = parse
         Output.end_inline_coq_block ();
         formatted := false;
         doc_list_bol indents lexbuf }
+  | "[[[" nl
+      { inf_rules (Some indents) lexbuf }
   | space* nl space* '-'
       { (* Like in the doc_bol production, these two productions
            exist only to deal properly with whitespace *)
@@ -769,9 +782,16 @@ and doc_list_bol indents = parse
                 backtrack_past_newline lexbuf;
                 doc_list_bol indents lexbuf
               end
-        | Before -> Output.stop_item ();
-                    backtrack_past_newline lexbuf;
-                    doc_bol lexbuf
+        | Before -> 
+        (* Here we were at the beginning of a line, and it was blank.
+           The next line started before any list items.  So: insert
+           a paragraph for the empty line, rewind to whatever's just
+           after the newline, then toss over to doc_bol for whatever
+           comes next. *)
+            Output.stop_item ();
+            Output.paragraph ();
+            backtrack_past_newline lexbuf;
+            doc_bol lexbuf
 
       }
   | space* _
@@ -780,7 +800,10 @@ and doc_list_bol indents = parse
         | Before -> Output.stop_item (); backtrack lexbuf;
                     doc_bol lexbuf
         | StartLevel n ->
-            Output.reach_item_level (n-1);
+            (if n = 1 then
+               Output.stop_item ()
+             else
+               Output.reach_item_level (n-1));
             backtrack lexbuf;
             doc (Some (take (n-1) indents)) lexbuf
         | InLevel (n,_) ->
@@ -808,8 +831,11 @@ and doc indents = parse
 		  | Some ls -> doc_list_bol ls lexbuf
 		  | None -> doc_bol lexbuf
 		else doc indents lexbuf)}
+  | "[[[" nl
+      { inf_rules indents lexbuf }
   | "[]"
       { Output.proofbox (); doc indents lexbuf }
+  | "{{" { url lexbuf; doc indents lexbuf }
   | "["
       { if !Cdglobals.plain_comments then Output.char '['
         else (brackets := 1;  Output.start_inline_coq (); escaped_coq lexbuf;
@@ -823,6 +849,18 @@ and doc indents = parse
         let eol = comment lexbuf in
           if eol then bol_parse lexbuf else doc indents lexbuf
       }
+  | '*'* "*)" space_nl* "(**"
+      {(match indents with
+        | Some _ -> Output.stop_item ()
+        | None -> ());
+       (* this says - if there is a blank line between the two comments,
+          insert one in the output too *)
+       let lines = List.length (Str.split_delim (Str.regexp "['\n']") 
+                                                (lexeme lexbuf))
+       in 
+         if lines > 2 then Output.paragraph ();
+       doc_bol lexbuf
+      }
   | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
@@ -857,6 +895,15 @@ and doc indents = parse
       { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ;
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
+  | "<<" space*
+      { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+  | '"'
+      { if !Cdglobals.plain_comments 
+	then Output.char '"' 
+	else if in_quote ()
+	then stop_quote () 
+	else start_quote ();
+        doc indents lexbuf }
   | eof
       { false }
   | _
@@ -883,11 +930,22 @@ and escaped_html = parse
   | eof { () }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
-and verbatim = parse
-  | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | eof { Output.stop_verbatim () }
-  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim 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 }
+  | eof { Output.stop_verbatim inline }
+  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
+
+and url = parse
+  | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
+  | "}" { url_name lexbuf }
+  | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf }
+
+and url_name = parse
+  | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer));
+	  Buffer.clear url_buffer; Buffer.clear url_name_buffer }
+  | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf }
 
 (*s Coq, inside quotations *)
 
@@ -911,10 +969,16 @@ and escaped_coq = parse
       { Tokens.flush_sublexer();
         Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
         escaped_coq lexbuf }
-  | space
-      { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
-        escaped_coq lexbuf }
-  | _
+  | space_nl*
+      { let str = lexeme lexbuf in
+          Tokens.flush_sublexer();
+          (if !Cdglobals.inline_notmono then () 
+                                        else Output.end_inline_coq ()); 
+          String.iter Output.char str; 
+          (if !Cdglobals.inline_notmono then () 
+                                        else Output.start_inline_coq ());
+          escaped_coq lexbuf }
+  | _ 
       { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
         escaped_coq lexbuf }
 
@@ -1081,7 +1145,7 @@ and body = parse
 	     if eol
 	     then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }
-  | "where" space*
+  | "where" 
       { Tokens.flush_sublexer();
         Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
 	start_notation_string lexbuf }
@@ -1105,6 +1169,8 @@ and body = parse
         body lexbuf }
 
 and start_notation_string = parse
+  | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
+	    start_notation_string lexbuf }
   | '"' (* a true notation *)
       { Output.sublexer '"' (lexeme_start lexbuf);
         notation_string lexbuf;
@@ -1141,6 +1207,71 @@ and printing_token_body = parse
   | _   { Buffer.add_string token_buffer (lexeme lexbuf);
 	  printing_token_body lexbuf }
 
+(*s These handle inference rules, parsing the body segments of things
+    enclosed in [[[  ]]] brackets *)
+and inf_rules indents = parse
+  | space* nl     (* blank line, before or between definitions *)
+      { inf_rules indents lexbuf }
+  | "]]]" nl      (* end of the inference rules block *)
+      { match indents with
+        | Some ls -> doc_list_bol ls lexbuf
+        | None -> doc_bol lexbuf }
+  | _ 
+      { backtrack lexbuf;  (* anything else must be the first line in a rule *)
+        inf_rules_assumptions indents [] lexbuf}
+
+(* The inference rule parsing just collects the inference rule and then
+   calls the output function once, instead of doing things incrementally
+   like the rest of the lexer.  If only there were a real parsing phase...
+*)
+and inf_rules_assumptions indents assumptions = parse
+  | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let dashes_and_name = 
+               cut_head_tail_spaces (String.sub line 0 (String.length line - 1))
+        in
+        let ldn = String.length dashes_and_name in
+        let (dashes,name) = 
+          try (let i = String.index dashes_and_name ' ' in
+               let d = String.sub dashes_and_name 0 i in
+               let n = cut_head_tail_spaces 
+                        (String.sub dashes_and_name (i+1) (ldn-i-1))
+               in
+                 (d, Some n))
+          with _ -> (dashes_and_name, None)
+            
+        in
+          inf_rules_conclusion indents (List.rev assumptions) 
+                               (spaces, dashes, name) [] lexbuf }
+  | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let assumption = cut_head_tail_spaces 
+                            (String.sub line 0 (String.length line - 1))
+        in
+          inf_rules_assumptions indents ((spaces,assumption)::assumptions)
+                                lexbuf }
+
+(*s The conclusion is required to come immediately after the
+    horizontal bar.  It is allowed to contain multiple lines of
+    text, like the assumptions.  The conclusion ends when we spot a
+    blank line or a ']]]'. *)
+and inf_rules_conclusion indents assumptions middle conclusions = parse
+  | space* nl | space* "]]]" nl (* end of conclusions. *)
+      { backtrack lexbuf;
+        Output.inf_rule assumptions middle (List.rev conclusions);
+        inf_rules indents lexbuf }
+  | space* [^ '\n']+ nl (* this is a line in the conclusion *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let conc = cut_head_tail_spaces (String.sub line 0 
+                                                    (String.length line - 1))
+        in
+          inf_rules_conclusion indents assumptions middle 
+                               ((spaces,conc) :: conclusions) lexbuf
+      }
+
 (*s A small scanner to support the chapter subtitle feature *)
 and st_start m = parse
   | "(*" "*"+ space+ "*" space+
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index a2cb995e..14447b06 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Filename
 open Lexing
 open Printf
@@ -38,17 +35,18 @@ type entry_type =
 type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
-  | Mod of coq_module * string
 
 let current_type : entry_type ref = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
-(** [deftable] stores only definitions and is used to interpolate idents
-    inside comments, which are not globalized otherwise. *)
-
+(** [deftable] stores only definitions and is used to build the index *)
 let deftable = Hashtbl.create 97
 
+(** [byidtable] is used to interpolate idents inside comments, which are not
+    globalized otherwise. *)
+let byidtable = Hashtbl.create 97
+
 (** [reftable] stores references and definitions *)
 let reftable = Hashtbl.create 97
 
@@ -62,25 +60,25 @@ let full_ident sp id =
   else ""
 
 let add_def loc1 loc2 ty sp id =
+  let fullid = full_ident sp id in
+  let def = Def (fullid, ty) in
   for loc = loc1 to loc2 do
-    Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
+    Hashtbl.add reftable (!current_library, loc) def
   done;
-  Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+  Hashtbl.add deftable !current_library (fullid, ty);
+  Hashtbl.add byidtable id (!current_library, fullid, ty)
 
 let add_ref m loc m' sp id ty =
+  let fullid = full_ident sp id in
   if Hashtbl.mem reftable (m, loc) then ()
-  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+  else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty));
   let idx = if id = "<>" then m' else id in
-    if Hashtbl.mem deftable idx then ()
-    else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
-
-let add_mod m loc m' id =
-  Hashtbl.add reftable (m, loc) (Mod (m', id));
-  Hashtbl.add deftable m (Mod (m', id))
+    if Hashtbl.mem byidtable idx then ()
+    else Hashtbl.add byidtable idx (m', fullid, ty)
 
 let find m l = Hashtbl.find reftable (m, l)
 
-let find_string m s = Hashtbl.find deftable s
+let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
 (*s Manipulating path prefixes *)
 
@@ -238,18 +236,20 @@ let type_name = function
 let prepare_entry s = function
   | Notation ->
       (* We decode the encoding done in Dumpglob.cook_notation of coqtop *)
-      (* Encoded notations have the form section:sc:x_'++'_x where: *)
-      (* - the section, if any, ends with a "." *)
-      (* - the scope can be empty *)
-      (* - tokens are separated with "_" *)
-      (* - non-terminal symbols are conventionally represented by "x" *)
-      (* - terminals are enclosed within simple quotes *)
-      (* - existing simple quotes (that necessarily are parts of terminals) *)
-      (*   are doubled *)
+      (* Encoded notations have the form section:sc:x_'++'_x where:      *)
+      (* - the section, if any, ends with a "."                          *)
+      (* - the scope can be empty                                        *)
+      (* - tokens are separated with "_"                                 *)
+      (* - non-terminal symbols are conventionally represented by "x"    *)
+      (* - terminals are enclosed within simple quotes                   *)
+      (* - existing simple quotes (that necessarily are parts of         *)
+      (*   terminals) are doubled                                        *)
       (*   (as a consequence, when a terminal contains "_" or "x", these *)
       (*   necessarily appear enclosed within non-doubled simple quotes) *)
-      (*   Example: "x ' %x _% y %'x %'_' z" is encoded as *)
-      (*     "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *)
+      (* - non-printable characters < 32 are left encoded so that they   *)
+      (*   are human-readable in index files                             *)
+      (* Example: "x ' %x _% y %'x %'_' z" is encoded as                 *)
+      (*   "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x"                        *)
       let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
@@ -268,10 +268,10 @@ let prepare_entry s = function
 	  | _ -> assert false)
 	end
 	else
-	  if s.[!j] = '\'' then begin
-	    if (!j = l || s.[!j+1] <> '\'') then quoted := false
-	    else (ntn.[!k] <- s.[!j]; incr k; incr j)
-	  end else begin
+	  if s.[!j] = '\'' then
+	    if (!j = l || s.[!j+1] = '_') then quoted := false
+	    else (incr j; ntn.[!k] <- s.[!j]; incr k)
+	  else begin
 	    ntn.[!k] <- s.[!j];
 	    incr k
 	  end;
@@ -290,11 +290,8 @@ let all_entries () =
     let l = try Hashtbl.find bt t with Not_found -> [] in
       Hashtbl.replace bt t ((s,m) :: l)
   in
-  let classify (m,_) e = match e with
-    | Def (s,t) -> add_g s m t; add_bt t s m
-    | Ref _ | Mod _ -> ()
-  in
-    Hashtbl.iter classify reftable;
+  let classify m (s,t) = (add_g s m t; add_bt t s m) in
+    Hashtbl.iter classify deftable;
     Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
     { idx_name = "global";
       idx_entries = sort_entries !gl;
@@ -324,8 +321,27 @@ let type_of_string = function
   | "sec" -> Section
   | s -> raise (Invalid_argument ("type_of_string:" ^ s))
 
-let read_glob f =
+let ill_formed_glob_file f =
+  eprintf "Warning: ill-formed file %s (links will not be available)\n" f
+let outdated_glob_file f =
+  eprintf "Warning: %s not consistent with corresponding .v file (links will not be available)\n" f
+
+let correct_file vfile f c =
+  let s = input_line c in
+  if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then
+    (ill_formed_glob_file f; false)
+  else
+    let s = String.sub s 7 (String.length s - 7) in
+    match vfile, s with
+    | None, "NO" -> true
+    | Some _, "NO" -> ill_formed_glob_file f; false
+    | None, _ -> ill_formed_glob_file f; false
+    | Some vfile, s ->
+        s = Digest.to_hex (Digest.file vfile) || (outdated_glob_file f; false)
+
+let read_glob vfile f =
   let c = open_in f in
+  if correct_file vfile f c then
   let cur_mod = ref "" in
   try
     while true do
@@ -341,7 +357,16 @@ let read_glob f =
 		Scanf.sscanf s "R%d:%d %s %s %s %s"
 		  (fun loc1 loc2 lib_dp sp id ty ->
 		    for loc=loc1 to loc2 do
-		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty)
+		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty);
+
+                      (* Also add an entry for each module mentioned in [lib_dp],
+                       * to use in interpolation. *)
+                      ignore (List.fold_right (fun thisPiece priorPieces ->
+                                                let newPieces = match priorPieces with
+                                                                | "" -> thisPiece
+                                                                | _ -> thisPiece ^ "." ^ priorPieces in
+                                                add_ref !cur_mod loc "" "" newPieces Library;
+                                                newPieces) (Str.split (Str.regexp_string ".") lib_dp) "")
 		    done)
 	       with _ -> ())
 	  | _ ->
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index a009e9dc..0f62a086 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 
 type loc = int
@@ -36,10 +34,11 @@ val type_name : entry_type -> string
 type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
-  | Mod of coq_module * string
 
+(* Find what symbol coqtop said is located at loc in the source file *)
 val find : coq_module -> loc -> index_entry
 
+(* Find what data is referred to by some string in some coq module *)
 val find_string : coq_module -> string -> index_entry
 
 val add_module : coq_module -> unit
@@ -54,7 +53,7 @@ val add_external_library : string -> coq_module -> unit
 
 (*s Read globalizations from a file (produced by coqc -dump-glob) *)
 
-val read_glob : string -> unit
+val read_glob : Digest.t option -> string -> unit
 
 (*s Indexes *)
 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 23dadbc1..b33ec1f0 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
  *  - coq_module: chop ./// (arbitrary amount of slashes), not only "./"
@@ -53,6 +50,7 @@ let usage () =
   prerr_endline "  -p <string>          insert <string> in LaTeX preamble";
   prerr_endline "  --files-from <file>  read file names to process in <file>";
   prerr_endline "  --glob-from <file>   read globalization information from <file>";
+  prerr_endline "  --no-glob            don't use any globalization information (no links will be inserted at identifiers)";
   prerr_endline "  --quiet              quiet mode (default)";
   prerr_endline "  --verbose            verbose mode";
   prerr_endline "  --no-externals       no links to Coq standard library";
@@ -73,6 +71,7 @@ let usage () =
   prerr_endline "  --no-lib-name        don't display \"Library\" before library names in the toc";
   prerr_endline "  --lib-name <string>  call top level toc entries <string> instead of \"Library\"";
   prerr_endline "  --lib-subtitles      first line comments of the form (** * ModuleName : text *) will be interpreted as subtitles";
+  prerr_endline "  --inline-notmono     use a proportional width font for inline code (possibly with a different color)";
   prerr_endline "";
   exit 1
 
@@ -107,25 +106,6 @@ let check_if_file_exists f =
   end
 
 
-(*s Manipulations of paths and path aliases *)
-
-let normalize_path p =
-  (* We use the Unix subsystem to normalize a physical path (relative
-     or absolute) and get rid of symbolic links, relative links (like
-     ./ or ../ in the middle of the path; it's tricky but it
-     works... *)
-  (* Rq: Sys.getcwd () returns paths without '/' at the end *)
-  let orig = Sys.getcwd () in
-  Sys.chdir p;
-  let res = Sys.getcwd () in
-  Sys.chdir orig;
-  res
-
-let normalize_filename f =
-  let basename = Filename.basename f in
-  let dirname = Filename.dirname f in
-  normalize_path dirname, basename
-
 (* [paths] maps a physical path to a name *)
 let paths = ref []
 
@@ -303,6 +283,9 @@ let parse () =
     | ("-lib-subtitles" | "--lib-subtitles") :: rem ->
       Cdglobals.lib_subtitles := true;
       parse_rec rem
+    | ("-inline-notmono" | "--inline-notmono") :: rem ->
+      Cdglobals.inline_notmono := true;
+      parse_rec rem
 
     | ("-latin1" | "--latin1") :: rem ->
 	Cdglobals.set_latin1 (); parse_rec rem
@@ -341,6 +324,8 @@ let parse () =
 	glob_source := GlobFile f; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
+    | ("-no-glob" | "--no-glob") :: rem ->
+	glob_source := NoGlob; parse_rec rem
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
 	Cdglobals.externals := false; parse_rec rem
     | ("--external" | "-external") :: u :: logicalpath :: rem ->
@@ -350,7 +335,11 @@ let parse () =
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
     | ("--boot" | "-boot") :: rem ->
-	Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
+	Cdglobals.coqlib_path := normalize_path (
+          Filename.concat
+            (Filename.dirname Sys.executable_name)
+            Filename.parent_dir_name
+        ); parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
@@ -458,13 +447,13 @@ let gen_mult_files l =
     end
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
-let read_glob_file x =
-  try Index.read_glob x
-  with Sys_error s ->
-    eprintf "Warning: %s (links will not be available)\n" s
+let read_glob_file vfile f =
+  try Index.read_glob vfile f
+  with Sys_error s -> eprintf "Warning: %s (links will not be available)\n" s
 
 let read_glob_file_of = function
-  | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob")
+  | Vernac_file (f,_) ->
+      read_glob_file (Some f) (Filename.chop_extension f ^ ".glob")
   | Latex_file _ -> ()
 
 let index_module = function
@@ -486,7 +475,7 @@ let produce_document l =
   (match !Cdglobals.glob_source with
     | NoGlob -> ()
     | DotGlob -> List.iter read_glob_file_of l
-    | GlobFile f -> read_glob_file f);
+    | GlobFile f -> read_glob_file None f);
   List.iter index_module l;
   match !out_to with
     | StdOut ->
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index eefcfd11..0dc86bc8 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 open Index
 
@@ -32,24 +29,27 @@ let build_table l =
 
 let is_keyword =
   build_table
-    [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+    [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
-      "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
+      "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar";
+      "Guarded"; "Goal"; "Hint"; "Debug"; "On";
       "Hypothesis"; "Hypotheses";
-      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
+      "Implicit"; "Import"; "Inductive";
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
       "Module"; "Module Type"; "Declare Module"; "Include";
-      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
-      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+      "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";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
-      "Delimit"; "Bind"; "Open"; "Scope";
-      "Boxed"; "Unboxed"; "Inline";
+      "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
-      "subgoal";
-      "Opaque"; "Transparent";
+      "subgoal"; "subgoals"; "vm_compute";
+      "Opaque"; "Transparent"; "Time";
+      "Extraction"; "Extract";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -57,14 +57,20 @@ let is_keyword =
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      "fix"; "cofix";
       (* Ltac *)
-      "before"; "after"
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+      (* Notations *)
+      "level"; "associativity"; "no"
        ]
 
 let is_tactic =
   build_table
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
-      "elimtype"; "progress"; "setoid_rewrite";
+      "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
+      "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+      "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
       "set"; "assert"; "do"; "repeat";
@@ -73,8 +79,10 @@ let is_tactic =
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
       "pattern"; "intuition"; "congruence"; "fail"; "fresh";
-      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
-      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
+      "trivial"; "tauto"; "firstorder"; "ring";
+      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto";
+      "change"; "fold"; "hnf"; "lazy"; "simple"; "eexists"; "debug"; "idtac"; "first"; "type of"; "pose";
+      "eval"; "instantiate"; "until" ]
 
 (*s Current Coq module *)
 
@@ -118,9 +126,12 @@ let initialize_texmacs () =
 
 let token_tree_texmacs = ref (initialize_texmacs ())
 
+let token_tree_latex = ref Tokens.empty_ttree
+let token_tree_html = ref Tokens.empty_ttree
+
 let initialize_tex_html () =
   let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
-    List.fold_right (fun (s,l,l') (tt,tt') ->
+  let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') ->
       (Tokens.ttree_add tt s l,
        match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l'))
       [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
@@ -143,10 +154,9 @@ let initialize_tex_html () =
 	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
 	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
 	(* "fun", "\\ensuremath{\\lambda}" ? *)
-      ] (Tokens.empty_ttree,Tokens.empty_ttree)
-
-let token_tree_latex = ref (fst (initialize_tex_html ()))
-let token_tree_html = ref (snd (initialize_tex_html ()))
+      ] (Tokens.empty_ttree,Tokens.empty_ttree) in
+  token_tree_latex := tree_latex;
+  token_tree_html  := tree_html
 
 let add_printing_token s (t1,t2) =
   (match t1 with None -> () | Some t1 ->
@@ -182,10 +192,20 @@ module Latex = struct
 
   let push_in_preamble s = Queue.add s preamble
 
+  let utf8x_extra_support () =
+    printf "\n";
+    printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
+    printf "%%interpret utf8 characters but extra packages might have to be added\n";
+    printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
+    printf "%%Use coqdoc's option -p to add new packages.\n";
+    printf "\\usepackage{tipa}\n";
+    printf "\n"
+
   let header () =
     if !header_trailer then begin
       printf "\\documentclass[12pt]{report}\n";
       if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
+      if !inputenc = "utf8x" then utf8x_extra_support ();
       printf "\\usepackage[T1]{fontenc}\n";
       printf "\\usepackage{fullpage}\n";
       printf "\\usepackage{coqdoc}\n";
@@ -255,6 +275,12 @@ module Latex = struct
 	| '^' | '~' as c ->
 	    Buffer.add_char buff '\\'; Buffer.add_char buff c;
 	    Buffer.add_string buff "{}"
+        | '\'' ->
+            if i < String.length s - 1 && s.[i+1] = '\'' then begin
+              Buffer.add_char buff '\''; Buffer.add_char buff '{';
+              Buffer.add_char buff '}'
+            end else
+              Buffer.add_char buff '\''
 	| c ->
 	    Buffer.add_char buff c
       done;
@@ -276,9 +302,23 @@ module Latex = struct
 
   let stop_latex_math () = output_char '$'
 
-  let start_verbatim () = printf "\\begin{verbatim}"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
+    
+  let start_verbatim inline = 
+    if inline then printf "\\texttt{"
+    else printf "\\begin{verbatim}"
 
-  let stop_verbatim () = printf "\\end{verbatim}\n"
+  let stop_verbatim inline =
+    if inline then printf "}"
+    else printf "\\end{verbatim}\n"
+
+  let url addr name = 
+    printf "%s\\footnote{\\url{%s}}"
+      (match name with
+       | None -> ""
+       | Some n -> n)
+      addr
 
   let indentation n =
     if n == 0 then
@@ -287,9 +327,6 @@ module Latex = struct
       let space = 0.5 *. (float n) in
       printf "\\coqdocindent{%2.2fem}\n" space
 
-  let module_ref m s =
-    printf "\\coqdocmodule{%s}{%s}" m (escaped s)
-
   let ident_ref m fid typ s =
     let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
@@ -306,18 +343,20 @@ module Latex = struct
 	  printf "\\coqdoc%s{%s}" (type_name typ) s
 
   let defref m id ty s =
-    printf "\\coqdef{"; label_ident (m ^ "." ^ id);
-    printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s
+    if ty <> Notation then
+      (printf "\\coqdef{"; label_ident (m ^ "." ^ id);
+       printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s)
+    else
+      (* Glob file still not able to say the exact extent of the definition *)
+      (* so we currently renounce to highlight the notation location *)
+      (printf "\\coqdef{"; label_ident (m ^ "." ^ id);
+       printf "}{%s}{%s}" s s)
 
   let reference s = function
     | Def (fullid,typ) ->
 	defref (get_module false) fullid typ s
-    | Mod (m,s') when s = s' ->
-	module_ref m s
     | Ref (m,fullid,typ) ->
 	ident_ref m fullid typ s
-    | Mod _ ->
-	printf "\\coqdocvar{%s}" (escaped s)
 
   (*s The sublexer buffers symbol characters and attached
        uninterpreted ident and try to apply special translation such as,
@@ -330,13 +369,22 @@ module Latex = struct
     | Some ref -> reference s ref
     | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s
 
+  let last_was_in = ref false
+
   let sublexer c loc =
-    let tag =
-      try Some (Index.find (get_module false) loc) with Not_found -> None
-    in
-    Tokens.output_tagged_symbol_char tag c
+    if c = '*' && !last_was_in then begin
+      Tokens.flush_sublexer ();
+      output_char '*'
+    end else begin
+      let tag =
+        try Some (Index.find (get_module false) loc) with Not_found -> None
+      in
+      Tokens.output_tagged_symbol_char tag c
+    end;
+    last_was_in := false
 
   let initialize () =
+    initialize_tex_html ();
     Tokens.token_tree := token_tree_latex;
     Tokens.outfun := output_sublexer_string
 
@@ -345,7 +393,11 @@ module Latex = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "\\coqdockw{%s}" (translate s)
+
   let ident s loc =
+    last_was_in := s = "in";
     try
       let tag = Index.find (get_module false) loc in
       reference (translate s) tag
@@ -478,8 +530,7 @@ module Html = struct
 	end
 
   let trailer () =
-    if !header_trailer then
-      if !footer_file_spec then
+    if !header_trailer && !footer_file_spec then
 	let cin = Pervasives.open_in !footer_file in
 	  try
 	    while true do
@@ -487,14 +538,14 @@ module Html = struct
 		printf "%s\n" s
 	    done
 	  with End_of_file -> Pervasives.close_in cin
-      else
-	begin
-	  if !index && (get_module false) <> "Index" then
-	    printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
-	  printf "<hr/>This page has been generated by ";
-	  printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
-	  printf "</div>\n\n</div>\n\n</body>\n</html>"
-	end
+    else
+      begin
+        if !index && (get_module false) <> "Index" then
+          printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
+	printf "<hr/>This page has been generated by ";
+	printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
+	printf "</div>\n\n</div>\n\n</body>\n</html>"
+      end
 
   let start_module () =
     let ln = !lib_name in
@@ -547,17 +598,22 @@ module Html = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = printf "<pre>"
-  let stop_verbatim () = printf "</pre>\n"
+  let start_quote () = char '"'
+  let stop_quote () = start_quote ()
 
-  let module_ref m s =
-    match find_module m with
-      | Local ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External m when !externals ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External _ | Unknown ->
-	  output_string s
+  let start_verbatim inline = 
+    if inline then printf "<tt>"
+    else printf "<pre>"
+
+  let stop_verbatim inline = 
+    if inline then printf "</tt>" 
+    else printf "</pre>\n"
+
+  let url addr name = 
+    printf "<a href=\"%s\">%s</a>" addr 
+      (match name with
+       | Some n -> n
+       | None -> addr)
 
   let ident_ref m fid typ s =
     match find_module m with
@@ -575,12 +631,8 @@ module Html = struct
     | Def (fullid,ty) ->
 	printf "<a name=\"%s\">" fullid;
 	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
-    | Mod (m,s') when s = s' ->
-	module_ref m s
     | Ref (m,fullid,ty) ->
 	ident_ref m fullid (type_name ty) s
-    | Mod _ ->
-	printf "<span class=\"id\" type=\"mod\">%s</span>" s
 
   let output_sublexer_string doescape issymbchar tag s =
     let s = if doescape then escaped s else s in
@@ -597,12 +649,16 @@ module Html = struct
     Tokens.output_tagged_symbol_char tag c
 
   let initialize () =
+    initialize_tex_html();
     Tokens.token_tree := token_tree_html;
     Tokens.outfun := output_sublexer_string
 
   let translate s =
     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)
+
   let ident s loc =
     if is_keyword s then begin
       printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
@@ -624,7 +680,7 @@ module Html = struct
 
   let rec reach_item_level n =
     if !item_level < n then begin
-      printf "<ul>\n<li>"; incr item_level;
+      printf "<ul class=\"doclist\">\n<li>"; incr item_level;
       reach_item_level n
     end else if !item_level > n then begin
       printf "\n</li>\n</ul>\n"; decr item_level;
@@ -662,7 +718,9 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = printf "<span class=\"inlinecode\">"
+  let start_inline_coq () = 
+    if !inline_notmono then printf "<span class=\"inlinecodenm\">"
+                       else printf "<span class=\"inlinecode\">"
 
   let end_inline_coq () = printf "</span>"
 
@@ -670,7 +728,50 @@ module Html = struct
 
   let end_inline_coq_block () = end_inline_coq ()
 
-  let paragraph () = printf "\n<br/> <br/>\n"
+  let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n" 
+
+  (* inference rules *)
+  let inf_rule assumptions (_,_,midnm) conclusions =
+    (* this first function replaces any occurance of 3 or more spaces
+       in a row with "&nbsp;"s.  We do this to the assumptions so that
+       people can put multiple rules on a line with nice formatting *)
+    let replace_spaces str =
+      let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in 
+      let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in
+      let strs = List.map (fun r -> match r with
+                                    | Str.Text s  -> [s]
+                                    | Str.Delim s -> 
+                                        copy "&nbsp;" (String.length s))  
+                          results
+      in
+        String.concat "" (List.concat strs)
+    in
+    let start_assumption line =
+          (printf "<tr class=\"infruleassumption\">\n";
+           printf "  <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in
+    let end_assumption () =
+          (printf "  <td></td>\n";
+           printf "</td>\n") in
+    let rec print_assumptions hyps = 
+          match hyps with
+          | []                 -> start_assumption "&nbsp;&nbsp;"
+          | [(_,hyp)]          -> start_assumption hyp
+          | ((_,hyp) :: hyps') -> (start_assumption hyp;
+                                   end_assumption ();
+                                   print_assumptions hyps') in
+    printf "<center><table class=\"infrule\">\n";
+    print_assumptions assumptions;
+    printf "  <td class=\"infrulenamecol\" rowspan=\"3\">\n";
+    (match midnm with
+     | None   -> printf "    &nbsp;\n  </td>" 
+     | Some s -> printf "    %s &nbsp;\n  </td>" s);
+    printf "</tr>\n";
+    printf "<tr class=\"infrulemiddle\">\n";
+    printf "  <td class=\"infrule\"><hr /></td>\n";
+    printf "</tr>\n";
+    print_assumptions conclusions;
+    end_assumption ();
+    printf "</table></center>"
 
   let section lev f =
     let lab = new_label () in
@@ -858,19 +959,28 @@ module TeXmacs = struct
 
   let stop_latex_math () = output_char '>'
 
-  let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+  let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
+  let stop_verbatim inline = in_doc := false; printf "</verbatim>"
+
+  let url addr name = 
+    printf "%s<\\footnote><\\url>%s</url></footnote>" addr
+      (match name with
+       | None -> ""
+       | Some n -> n)
 
-  let stop_verbatim () = in_doc := false; printf "</verbatim>"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
 
   let indentation n = ()
 
+  let keyword s =
+    printf "<kw|"; raw_ident s; printf ">"
+
   let ident_true s =
-    if is_keyword s then begin
-      printf "<kw|"; raw_ident s; printf ">"
-    end else begin
-      raw_ident s
-    end
+    if is_keyword s then keyword s
+    else raw_ident s
 
+  let keyword s loc = keyword s
   let ident s _ = if !in_doc then ident_true s else raw_ident s
 
   let output_sublexer_string doescape issymbchar tag s =
@@ -985,13 +1095,21 @@ module Raw = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = ()
+  let start_verbatim inline = ()
+  let stop_verbatim inline = ()
 
-  let stop_verbatim () = ()
+  let url addr name = 
+    match name with
+    | Some n -> printf "%s (%s)" n addr
+    | None -> printf "%s" addr
+
+  let start_quote () = printf "\""
+  let stop_quote () = printf "\""
 
   let indentation n =
       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
@@ -1105,6 +1223,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
 let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp
 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 initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
@@ -1132,10 +1251,33 @@ let start_verbatim =
   select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
 let stop_verbatim =
   select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
-  select output_char Html.char TeXmacs.char Raw.char
+let verbatim_char inline =
+  select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
+let url = 
+  select Latex.url Html.url TeXmacs.url Raw.url
+
+let start_quote =
+  select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote
+let stop_quote =
+  select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
+
+let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = 
+  start_verbatim false;
+  let dumb_line = 
+       function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
+                            char '\n')
+  in 
+    (List.iter dumb_line assumptions;
+     dumb_line (midsp, midln ^ (match midnm with 
+                                | Some s -> " " ^ s 
+                                | None -> ""));
+     List.iter dumb_line conclusions);
+  stop_verbatim false
+
+let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb
+
 let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index
 let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index
 let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index dcd9072d..80f39011 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 open Index
 
@@ -62,6 +60,7 @@ val rule : unit -> unit
 
 val nbsp : unit -> unit
 val char : char -> unit
+val keyword : string -> loc -> unit
 val ident : string -> loc -> unit
 val sublexer : char -> loc -> unit
 val initialize : unit -> unit
@@ -72,13 +71,34 @@ val latex_char : char -> unit
 val latex_string : string -> unit
 val html_char : char -> unit
 val html_string : string -> unit
-val verbatim_char : char -> unit
+val verbatim_char : bool -> char -> unit
 val hard_verbatim_char : char -> unit
 
 val start_latex_math : unit -> unit
 val stop_latex_math : unit -> unit
-val start_verbatim : unit -> unit
-val stop_verbatim : unit -> unit
+val start_verbatim : bool -> unit
+val stop_verbatim : bool -> unit
+val start_quote : unit -> unit
+val stop_quote : unit -> unit
+
+val url : string -> string option -> unit
+
+(* this outputs an inference rule in one go.  You pass it the list of
+   assumptions, then the middle line info, then the conclusion (which
+   is allowed to span multiple lines).
+
+   In each case, the int is the number of spaces before the start of
+   the line's text and the string is the text of the line with the
+   leading trailing space trimmed.  For the middle rule, you can
+   also optionally provide a name.
+
+   We need the space info so that in modes where we aren't doing
+   something smart we can just format the rule verbatim like the user did
+*)
+val inf_rule :  (int * string) list
+             -> (int * string * (string option)) 
+             -> (int * string) list
+             -> unit
 
 val make_multi_index : unit -> unit
 val make_index : unit -> unit
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 9de39083..10a105f9 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-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index 3b756e18..e9c74307 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-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 380448be..a5376ec4 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,8 +9,6 @@
 (* coqwc - counts the lines of spec, proof and comments in Coq sources
  * Copyright (C) 2003 Jean-Christophe Filliâtre *)
 
-(*i $Id: coqwc.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
     It assumes the files to be lexically well-formed. *)
 
diff --git a/tools/escape_string.ml b/tools/escape_string.ml
new file mode 100644
index 00000000..50e8faad
--- /dev/null
+++ b/tools/escape_string.ml
@@ -0,0 +1 @@
+print_string (String.escaped Sys.argv.(1))
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
new file mode 100644
index 00000000..22a36ede
--- /dev/null
+++ b/tools/fake_ide.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** 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 (true,false,s)));
+    "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s)));
+    "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s)));
+    "INTERP", (fun s -> eval_call (Ide_intf.interp (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
+  in
+  find_cmd commands
+
+let usage () =
+  Printf.printf
+    "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
+
+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");
+  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
+  done
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 161d86a8..7b051d1c 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gallina.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Gallina_lexer
 
 let vfiles = ref ([] : string list)
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 638d5936..cfbfac98 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gallina_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 {
  open Lexing
 
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
new file mode 100644
index 00000000..f01b62cc
--- /dev/null
+++ b/tools/mingwpath.ml
@@ -0,0 +1,15 @@
+(** 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/win32hack.mllib b/tools/win32hack.mllib
new file mode 100644
index 00000000..42395f65
--- /dev/null
+++ b/tools/win32hack.mllib
@@ -0,0 +1 @@
+Win32hack_filename
\ No newline at end of file
diff --git a/tools/win32hack_filename.ml b/tools/win32hack_filename.ml
new file mode 100644
index 00000000..74f70686
--- /dev/null
+++ b/tools/win32hack_filename.ml
@@ -0,0 +1,4 @@
+(* The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
+   Let's tweak that... *)
+
+let _ = Filename.dir_sep.[0] <- '\\'