Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

12 files changed, 837 insertions, 385 deletions

diff --git a/tools/beautify-archive b/tools/beautify-archive
new file mode 100755
index 00000000..aac6f3e0
--- /dev/null
+++ b/tools/beautify-archive
@@ -0,0 +1,52 @@
+#!/bin/sh
+
+#This script compiles and beautifies an archive, check the correctness
+#of beautified files, then replace the original files by the
+#beautified ones, keeping a copy of original files in $OLDARCHIVE.
+#The script assumes:
+#- that the archive provides a Makefile built by coq_makefile,
+#- that coqc is in the path or that variables COQTOP and COQBIN are set.
+
+OLDARCHIVE=old_files
+NEWARCHIVE=beautify_files
+BEAUTIFYSUFFIX=.beautified
+
+if [ -e $OLDARCHIVE ]; then
+  echo "Warning: $OLDARCHIVE directory found, the files are maybe already beautified";
+  sleep 5;
+fi
+echo ---- Producing beautified files in the beautification directory -------
+if [ -e $NEWARCHIVE ]; then rm -r $NEWARCHIVE; fi
+if [ -e /tmp/$OLDARCHIVE.$$ ]; then rm -r /tmp/$OLDARCHIVE.$$; fi
+cp -pr . /tmp/$OLDARCHIVE.$$
+cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE
+cd $NEWARCHIVE
+rm description || true
+make clean
+make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+ { echo ---- Failed to beautify; exit 1; }
+echo -------- Upgrading files in the beautification directory --------------
+beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX`
+for i in $beaufiles; do
+  j=`dirname $i`/`basename $i .v$BEAUTIFYSUFFIX`.v
+  echo Upgrading $j in the beautification directory
+  mv -u -f $i $j
+done
+echo ---- Recompiling beautified files in the beautification directory -----
+make clean
+make || { echo ---- Failed to recompile; exit 1; }
+echo ----- Saving old files in directory $OLDARCHIVE -------------------------
+/bin/rm -r ../$OLDARCHIVE
+mv /tmp/$OLDARCHIVE.$$ ../$OLDARCHIVE
+echo Saving $OLDARCHIVE files done
+echo --------- Upgrading files in current directory ------------------------
+vfiles=`find . -name \*.v`
+cd ..
+for i in $vfiles; do
+  echo Upgrading $i in current directory
+  mv -u -f $NEWARCHIVE/$i $i
+done
+echo -------- Beautification completed -------------------------------------
+echo Old files are in directory '"$OLDARCHIVE"'
+echo New files are in current directory
+echo You can now remove the beautification directory '"$NEWARCHIVE"'
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index d1d0d854..3fbf71dd 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 11255 2008-07-24 16:57:13Z notin $ *)
+(* $Id: coq_makefile.ml4 11771 2009-01-09 18:00:56Z notin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -29,6 +29,7 @@ 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
@@ -38,6 +39,14 @@ let rec print_list sep = function
   | 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) '#'
@@ -58,10 +67,11 @@ let usage () =
 
 coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
   command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath]
-  ... [VARIABLE = value] ...  [-opt|-byte] [-f file] [-o file] [-h] [--help]
+  ... [VARIABLE = value] ...  [-opt|-byte] [-impredicative-set] [-no-install]
+  [-f file] [-o file] [-h] [--help]
 
 [file.v]: Coq file to be compiled
-[file.ml]: ML 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\"
@@ -73,26 +83,118 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
 [-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 standard sds sps =
+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";
+  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 $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" 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 $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" 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 $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
+    printf "\t done)\n"
+
+let install (vfiles,mlfiles,_,sds) inc =
   print "install:\n";
-  print "\tmkdir -p `$(COQC) -where`/user-contrib\n";
-  if !some_vfile then print "\tcp -f $(VOFILES) `$(COQC) -where`/user-contrib\n";
-  if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\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 -> print "\t(cd "; print x; print " ; $(MAKE) install)\n")
+    (fun x ->
+      printf "\t(cd %s; $(MAKE) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x)
     sds;
-  print "\n";
+  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;
@@ -102,16 +204,22 @@ let standard sds sps =
       (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n")
       sds;
     print "\n";
-  end;
+  end
+
+let clean sds sps =
   print "clean:\n";
-  print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n";
-  print "\trm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
+  print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) *~\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)\n";
+  if Coq_config.has_natdynlink && !some_mlfile then
+    print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n";
   print "\t- rm -rf html\n";
   List.iter
-    (fun (file,_,_) -> print "\t- rm -f "; print file; print "\n")
+    (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")
@@ -122,19 +230,26 @@ let standard sds sps =
   List.iter
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
     sds;
-  print "\n\n"
+  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 includes () =
+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 "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
+    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
+    print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(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 "%.ml.d: %.ml\n";
-    print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n"
+    print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n"
   and v_rule () =
     print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -149,34 +264,10 @@ let implicit () =
     if !some_mlfile then ml_rules ();
     if !some_vfile then v_rule ()
 
-let variables l =
-  let rec var_aux = function
-    | [] -> ()
-    | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r
-    | _ :: r -> var_aux r
-  in
+let variables defs =
+  let var_aux (v,def) = print v; print "="; print def; print "\n" in
     section "Variables definitions.";
-    print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; 
-    if Coq_config.local then
-      (print "COQSRC:=$(COQTOP)\n";
-       print "COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
-  -I $(COQTOP)/library -I $(COQTOP)/parsing \\
-  -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
-  -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\
-  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc \\
-  -I $(COQTOP)/contrib/dp -I $(COQTOP)/contrib/extraction \\
-  -I $(COQTOP)/contrib/field -I $(COQTOP)/contrib/firstorder \\
-  -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/funind \\
-  -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\
-  -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\
-  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\
-  -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\
-  -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\
-  -I $(CAMLP4LIB)\n")
-    else
-      (print "COQSRC:=$(shell $(COQBIN)coqc -where)\n"; 
-       print "COQSRCLIBS:=-I $(COQSRC)\n");
-    print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n";
+    print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n";
     if !opt = "-byte" then 
       print "override OPT:=-byte\n"
     else
@@ -184,81 +275,62 @@ let variables l =
     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 "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n";
-    printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c\n";
-    printf "CAMLLINK:=$(CAMLBIN)ocamlc -rectypes\n";
-    printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes\n";
+    printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
+    printf "CAMLOPTC:=$(CAMLBIN)%s -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";
-
-    (if Coq_config.local then
-      print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"
-    else
-      print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQSRC) $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"); 
-    var_aux l;
+    print "CAMLP4OPTIONS:=\n";
+    List.iter var_aux defs;
+    print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n";
     print "\n"
 
-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 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 is_included dir = function
-  | RInclude (dir',_) -> is_prefix (absolute_dir dir') (absolute_dir dir)
-  | Include dir' -> absolute_dir dir = absolute_dir dir'
-  | _ -> false
-
-let dir_of_target t = 
-  match t with
-    | RInclude (dir,_) -> dir
-    | Include dir -> dir
-    | _ -> assert false
-
-let include_dirs l =
-  let rec split_includes l = 
-    match l with
-      | [] -> [], []
-      | Include _ as i :: rem ->
-	  let ri, rr = split_includes rem in 
-	    (i :: ri), rr
-      | RInclude _ as r :: rem -> 
-	  let ri, rr = split_includes rem in 
-	    ri, (r :: rr)
-      | _ :: rem -> split_includes rem
-  in
-  let rec parse_includes l = 
-    match l with
-      | [] -> []
-      | Include x :: rem -> ("-I " ^ x) :: parse_includes rem
-      | RInclude (p,l) :: rem ->
-	  let l' = if l = "" then "\"\"" else l in
-            ("-R " ^ p ^ " " ^ l') :: parse_includes rem
-      | _ :: rem -> parse_includes rem
-  in
-  let l' = if List.exists (is_included ".") l then l else Include "." :: l in
-  let inc_i, inc_r = split_includes l' in
-  let inc_i' = List.filter (fun i -> not (List.exists (fun i' -> is_included (dir_of_target i) i') inc_r)) inc_i in 
+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_includes inc_r in
-    section "Libraries definition.";
-    print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
+  let str_r = parse_rec_includes inc_r in
+    section "Libraries definitions.";
     print "OCAMLLIBS:=-I $(CAMLP4LIB) "; 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 -I $(COQLIB)/contrib/cc -I $(COQLIB)/contrib/dp \\
+  -I $(COQLIB)/contrib/extraction -I $(COQLIB)/contrib/field \\
+  -I $(COQLIB)/contrib/firstorder -I $(COQLIB)/contrib/fourier \\
+  -I $(COQLIB)/contrib/funind -I $(COQLIB)/contrib/interface \\
+  -I $(COQLIB)/contrib/micromega -I $(COQLIB)/contrib/omega \\
+  -I $(COQLIB)/contrib/ring -I $(COQLIB)/contrib/romega \\
+  -I $(COQLIB)/contrib/rtauto -I $(COQLIB)/contrib/setoid_ring \\
+  -I $(COQLIB)/contrib/subtac -I $(COQLIB)/contrib/xml\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)
@@ -272,15 +344,10 @@ let custom sps =
     if sps <> [] then section "Custom targets.";
     List.iter pr_sp sps
 
-let subdirs l =
-  let rec subdirs_aux = function
-    | [] -> []
-    | Subdir x :: r -> x :: (subdirs_aux r)
-    | _ :: r -> subdirs_aux r
-  and pr_subdir s =
+let subdirs sds =
+  let pr_subdir s =
     print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n"
   in
-  let sds = subdirs_aux l in
     if sds <> [] then section "Subdirectories.";
     List.iter pr_subdir sds;
     section "Special targets.";
@@ -288,30 +355,31 @@ let subdirs l =
     print_list " "
       ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install" 
 	:: "depend" :: "html" :: sds);
-    print "\n\n";
-    sds
-
-
-let all_target l =
-  let rec parse_arguments l = 
-    match l with
-      | ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o)
-      | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
-      | V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o)
-      | Special (n,_,_) :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
-      | Include _ :: r -> parse_arguments r
-      | RInclude _ :: r -> parse_arguments r
-      | Def _ :: r -> parse_arguments r
-      | [] -> [],[],[]
-  in
-  let 
-      vfiles, mlfiles, other_targets = parse_arguments l
-  in
-    section "Definition of the \"all\" target.";
+    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";
@@ -322,10 +390,18 @@ let all_target l =
       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
@@ -341,8 +417,20 @@ let all_target l =
 	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 
@@ -379,14 +467,14 @@ let rec process_cmd_line = function
       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" then
+	else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then
           some_mlfile := true
-	else
-	  () 
       in
 	List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies);
 	Special (file,dependencies,com) :: (process_cmd_line r)
@@ -411,11 +499,14 @@ let rec process_cmd_line = function
       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" then begin
-            some_mlfile := true; 
-	    ML f :: (process_cmd_line r)
-      end else
-            Subdir 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
@@ -462,24 +553,61 @@ let directories_deps 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 subdirectoty 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
-    banner ();
-    warning ();
-    command_line args;
-    include_dirs l;
-    variables l;
-    all_target l;
-    let sps = special  l in
-      custom sps;
-      let sds = subdirs l in
-	implicit ();
-	standard sds sps;
-	(* TEST directories_deps l; *)
-	includes ();
-	warning ();
-	if not (!output_channel == stdout) then close_out !output_channel;
-	exit 0
+  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 =
@@ -489,4 +617,3 @@ let main () =
     do_makefile args
       
 let _ = Printexc.catch main ()
-
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index b4b161f5..4febe9d1 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: coqdep.ml 11749 2009-01-05 14:01:04Z notin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -15,8 +15,6 @@ open Unix
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
-let coqlib = ref Coq_config.coqlib
-
 let option_c = ref false
 let option_D = ref false
 let option_w = ref false
@@ -24,7 +22,6 @@ let option_i = ref false
 let option_sort = ref false
 let option_glob = ref false
 let option_slash = ref false
-let option_boot = ref false
 
 let suffixe = ref ".vo"
 let suffixe_spec = ref ".vi"
@@ -245,7 +242,11 @@ let traite_fichier_Coq verbose f =
 			addQueue deja_vu_ml s;
                	       try
               		 let mldir = Hashtbl.find mlKnown s in
-              		   printf " %s.cmo" (file_name ([String.uncapitalize s],mldir))
+			 let filename = file_name ([String.uncapitalize s],mldir) in
+              		 if Coq_config.has_natdynlink then
+			   printf " %s.cmo %s.cmxs" filename filename
+			 else
+			   printf " %s.cmo" filename
               	       with Not_found -> ()
 		     end)
 		sl
@@ -501,14 +502,14 @@ let rec parse = function
   | "-D" :: ll -> option_D := true; parse ll
   | "-w" :: ll -> option_w := true; parse ll
   | "-i" :: ll -> option_i := true; parse ll
-  | "-boot" :: ll -> option_boot := true; parse ll
+  | "-boot" :: ll -> Flags.boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | "-glob" :: ll -> option_glob := true; parse ll
   | "-I" :: r :: ll -> add_dir add_known r []; parse ll
   | "-I" :: [] -> usage ()
   | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
   | "-R" :: ([] | [_]) -> usage ()
-  | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll
+  | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
   | "-suffix" :: [] -> usage ()
@@ -519,13 +520,14 @@ let rec parse = function
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   parse (List.tl (Array.to_list Sys.argv));
-  if !option_boot then begin
+  if !Flags.boot then begin
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "contrib" ["Coq"]
-  end else begin 
-    add_rec_dir add_coqlib_known (!coqlib//"theories") ["Coq"]; 
-    add_rec_dir add_coqlib_known (!coqlib//"contrib") ["Coq"];
-    add_dir add_coqlib_known (!coqlib//"user-contrib") []
+  end else begin
+    let coqlib = Envars.coqlib () in
+      add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; 
+      add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"];
+      add_dir add_coqlib_known (coqlib//"user-contrib") []
   end;
   List.iter (fun (f,_,d) -> Hashtbl.add mliKnown f d) !mliAccu;
   List.iter (fun (f,_,d) -> Hashtbl.add mlKnown f d) !mlAccu;
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 3339b1db..5bcbed64 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -10,7 +10,7 @@
 
 (*s Output options *)
 
-type target_language = LaTeX | HTML | TeXmacs
+type target_language = LaTeX | HTML | TeXmacs | Raw
 
 let target_language = ref HTML
 
@@ -57,6 +57,7 @@ let externals = ref true
 let coqlib = ref "http://coq.inria.fr/library/"
 let coqlib_path = ref Coq_config.coqlib
 let raw_comments = ref false
+let interpolate = ref false
 
 let charset = ref "iso-8859-1"
 let inputenc = ref ""
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 65c39b7a..a9a99706 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -25,7 +25,7 @@ body { padding: 0px 0px;
        padding: 10px;
        overflow: hidden;
        font-size: 100%;
-       line-height: 80% }
+       line-height: 100% }
 
 #main  a.idref:visited {color : #416DFF; text-decoration : none; }
 #main  a.idref:link {color : #416DFF; text-decoration : none; }
@@ -43,8 +43,6 @@ body { padding: 0px 0px;
 #main .section { background-color:#90bdff;
                  font-size : 175% }
 
-#main code { font-family: monospace }
-
 #main .doc { margin: 0px;
              padding: 10px;
              font-family: sans-serif;
@@ -55,7 +53,13 @@ body { padding: 0px 0px;
              background-color: #90bdff;
              border-style: plain}
 
-#main .doc code { font-family: monospace} 
+.inlinecode { 
+    display: inline;
+    font-family: monospace } 
+
+.code { 
+    display: block;
+    font-family: monospace } 
 
 /* Pied de page */
 
@@ -66,3 +70,29 @@ body { padding: 0px 0px;
 #footer a:link { text-decoration: none; 
                  color: #888888; }
 
+.id { display: inline; }
+
+.id[type="constructor"] { 
+    color: rgb(60%,0%,0%);
+}
+
+.id[type="var"] { 
+    color: rgb(40%,0%,40%);
+}
+
+.id[type="definition"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="lemma"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="inductive"] { 
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="keyword"] { 
+ color : #cf1d1d;
+/*     color: black; */
+}
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index d31314c5..ef4f4119 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -27,6 +27,11 @@
 %HEVEA\renewcommand{\medskip}{}
 %HEVEA\renewcommand{\bigskip}{}
 
+
+%HEVEA\newcommand{\lnot}{\coqwkw{not}}
+%HEVEA\newcommand{\lor}{\coqwkw{or}}
+%HEVEA\newcommand{\land}{\&}
+
 % own name
 \newcommand{\coqdoc}{\textsf{coqdoc}}
 
@@ -39,7 +44,7 @@
 \newcommand{\coqdockw}[1]{\texttt{#1}}
 
 % macro for typesetting variable identifiers
-\newcommand{\coqdocid}[1]{\textit{#1}}
+\newcommand{\coqdocvar}[1]{\textit{#1}}
 
 % macro for typesetting constant identifiers
 \newcommand{\coqdoccst}[1]{\textsf{#1}}
@@ -57,52 +62,93 @@
 % macro for typesetting constructor identifiers
 \newcommand{\coqdocconstr}[1]{\textsf{#1}}
 
+% macro for typesetting tactic identifiers
+\newcommand{\coqdoctac}[1]{\texttt{#1}}
+
+
+% Environment encompassing code fragments
+% !!! CAUTION: This environment may have empty contents
+\newenvironment{coqdoccode}{}{}
+
 % newline and indentation 
 %BEGIN LATEX
-\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par}
-\newcommand{\coqdocindent}[1]{\noindent\kern#1}
-%END LATEX
-%HEVEA\newcommand{\coqdoceol}{\begin{rawhtml}<BR>\end{rawhtml}}
-%HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}}
+% Base indentation length
+\newlength{\coqdocbaseindent}
+\setlength{\coqdocbaseindent}{0em}
+
+% Beginning of a line without any Coq indentation
+\newcommand{\coqdocnoindent}{\noindent\kern\coqdocbaseindent}
+% Beginning of a line with a given Coq indentation
+\newcommand{\coqdocindent}[1]{\noindent\kern\coqdocbaseindent\noindent\kern#1}
+% End-of-the-line
+\newcommand{\coqdoceol}{\hspace*{\fill}\setlength\parskip{0pt}\par}
+% Empty lines (in code only)
+\newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em}
 
 % macro for typesetting the title of a module implementation
 \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
 }
 \usepackage{ifpdf}
 \ifpdf
-  \usepackage[pdftex]{hyperref}
+  \RequirePackage{hyperref}
   \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}
-  \usepackage[all]{hypcap}
+
+  % To do indexing, use something like:
+  % \usepackage{multind}
+  % \newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
 
   \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
   \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
   \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
   \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
-    \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}}
+    \hypertarget{coq:#1}{\chapter{Library \texorpdfstring{\coqdoccst}{}{#2}}}}
 \else
   \newcommand{\coqdef}[3]{#3}
   \newcommand{\coqref}[2]{#2}
-  \newcommand{\identref}[2]{\textsf {#2}}
+  \newcommand{\texorpdfstring}[2]{#1}
+  \newcommand{\identref}[2]{\textsf{#2}}
   \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
 \fi
 \usepackage{xr}
 
-%\usepackage{color}
-%\usepackage{multind}
-%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
-
-  
-
-\newcommand{\coqdocvar}[1]{{\textit{#1}}}
-\newcommand{\coqdoctac}[1]{{\texttt{#1}}}
-
+\newif\if@coqdoccolors
+  \@coqdoccolorsfalse
+
+\DeclareOption{color}{\@coqdoccolorstrue}
+\ProcessOptions
+
+\if@coqdoccolors
+\RequirePackage{xcolor}
+\definecolor{varpurple}{rgb}{0.4,0,0.4}
+\definecolor{constrmaroon}{rgb}{0.6,0,0}
+\definecolor{defgreen}{rgb}{0,0.4,0}
+\definecolor{indblue}{rgb}{0,0,0.8}
+\definecolor{kwred}{rgb}{0.8,0.1,0.1}
+
+\def\coqdocvarcolor{varpurple}
+\def\coqdockwcolor{kwred}
+\def\coqdoccstcolor{defgreen}
+\def\coqdocindcolor{indblue}
+\def\coqdocconstrcolor{constrmaroon}
+\def\coqdocmodcolor{defgreen}
+\def\coqdocaxcolor{varpurple}
+\def\coqdoctaccolor{black}
+
+\def\coqdockw#1{{\color{\coqdockwcolor}{\texttt{#1}}}}
+\def\coqdocvar#1{{\color{\coqdocvarcolor}{\textit{#1}}}}
+\def\coqdoccst#1{{\color{\coqdoccstcolor}{\textrm{#1}}}}
+\def\coqdocind#1{{\color{\coqdocindcolor}{\textsf{#1}}}}
+\def\coqdocconstr#1{{\color{\coqdocconstrcolor}{\textsf{#1}}}}
+\def\coqdocmod#1{{{\color{\coqdocmodcolor}{\textsc{\textsf{#1}}}}}}
+\def\coqdocax#1{{{\color{\coqdocaxcolor}{\textsl{\textrm{#1}}}}}}
+\def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}}
+\fi
 
 \newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
 \newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
 
-%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
-%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
-\newcommand{\coqvariable}[2]{\coqdocid{#2}}
+\newcommand{\coqvariable}[2]{\coqdocvar{#2}}
+\newcommand{\coqvariableref}[2]{\coqref{#1}{\coqdocvar{#2}}}
 
 \newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
 \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
@@ -133,8 +179,8 @@
 
 \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
 
-\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+\newcommand{\coqsection}[2]{\coqdef{sec:#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqsectionref}[2]{\coqref{sec:#1}{\coqdoccst{#2}}}
 
 %\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
   
@@ -145,11 +191,7 @@
 \newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
 \newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
 
-\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}}
-\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}}
-
-
-%HEVEA\newcommand{\lnot}{\coqwkw{not}}
-%HEVEA\newcommand{\lor}{\coqwkw{or}}
-%HEVEA\newcommand{\land}{\&}
+\newcommand{\coqmodule}[2]{\coqdef{mod:#1}{#2}{\coqdocmod{#2}}}
+\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}}
 
+\endinput
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 1da8ebd7..56a3cd11 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mli 11065 2008-06-06 22:39:43Z msozeau $ i*)
+(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 open Cdglobals
 
@@ -40,6 +40,8 @@ type index_entry =
 
 val find : coq_module -> loc -> index_entry
 
+val find_string : coq_module -> string -> index_entry
+
 val add_module : coq_module -> unit
 
 type module_kind = Local | Coqlib | Unknown
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index fc2090dc..f8adb52b 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mll 11065 2008-06-06 22:39:43Z msozeau $ i*)
+(*i $Id: index.mll 11790 2009-01-15 20:19:58Z msozeau $ i*)
 
 {
 
@@ -47,9 +47,14 @@ let current_type = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
-let table = Hashtbl.create 97
-  (** [table] is used to store references and definitions *)
+(** [deftable] stores only definitions and is used to interpolate idents 
+    inside comments, which are not globalized otherwise. *)
 
+let deftable = Hashtbl.create 97
+
+(** [reftable] stores references and definitions *)
+let reftable = Hashtbl.create 97
+  
 let full_ident sp id =
   if sp <> "<>" then 
     if id <> "<>" then 
@@ -60,15 +65,24 @@ let full_ident sp id =
   else ""
     
 let add_def loc ty sp id = 
-  Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
-
+  Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
+  Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+    
 let add_ref m loc m' sp id ty = 
-  Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty))
+  if Hashtbl.mem reftable (m, loc) then ()
+  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, 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 table (m, loc) (Mod (m', id))
-
-let find m l = Hashtbl.find table (m, l)
-
+let add_mod m loc m' id = 
+  Hashtbl.add reftable (m, loc) (Mod (m', id));
+  Hashtbl.add deftable m (Mod (m', id))
+    
+let find m l = Hashtbl.find reftable (m, l)
+  
+let find_string m s = Hashtbl.find deftable s
+  
 (*s Manipulating path prefixes *) 
 
 type stack = string list 
@@ -216,7 +230,7 @@ let all_entries () =
     | Def (s,t) -> add_g s m t; add_bt t s m
     | Ref _ | Mod _ -> ()
   in
-    Hashtbl.iter classify table;
+    Hashtbl.iter classify reftable;
     Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
     { idx_name = "global"; 
       idx_entries = sort_entries !gl; 
@@ -238,7 +252,9 @@ let firstchar =
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
      '\'' '0'-'9']
-let ident = firstchar identchar*
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let ident = id | pfx_id id
 
 let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
 let end_hide = "(*" space* "end" space+ "hide" space* "*)"
@@ -406,9 +422,9 @@ and module_refs = parse
   | ident  
       { let id =  lexeme lexbuf in
 	  (try
-	      add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
-	    with
-		Not_found -> ()
+	     add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
+	   with
+	       Not_found -> ()
 	  ); 
 	module_refs lexbuf }
   | eof    
@@ -418,7 +434,7 @@ and module_refs = parse
 
 {
   let type_of_string = function
-    | "def" | "coe" | "subclass" | "canonstruc" 
+    | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
     | "ex" | "scheme" -> Definition
     | "prf" | "thm" -> Lemma
     | "ind" | "coind" -> Inductive
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 81560259..2e97618b 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 11236 2008-07-18 15:58:12Z notin $ i*)
+(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -30,6 +30,7 @@ let usage () =
   prerr_endline "  --html               produce a HTML document (default)";
   prerr_endline "  --latex              produce a LaTeX document";
   prerr_endline "  --texmacs            produce a TeXmacs document";
+  prerr_endline "  --raw                produce a text document";
   prerr_endline "  --dvi                output the DVI";
   prerr_endline "  --ps                 output the PostScript";
   prerr_endline "  --pdf                output the Pdf";
@@ -56,12 +57,14 @@ let usage () =
   prerr_endline "  --no-externals       no links to Coq standard library";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
   prerr_endline "                       (default is http://coq.inria.fr/library/)";
+  prerr_endline "  --boot               run in boot mode";
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  --latin1             set ISO-8859-1 input language";
   prerr_endline "  --utf8               set UTF-8 input language";
   prerr_endline "  --charset <string>   set HTML charset";
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
+  prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
   prerr_endline "";
   exit 1
 
@@ -81,6 +84,7 @@ let banner () =
 let target_full_name f = 
   match !Cdglobals.target_language with
     | HTML -> f ^ ".html"
+    | Raw -> f ^ ".txt"
     | _ -> f ^ ".tex"
 	
 (*s \textbf{Separation of files.} Files given on the command line are
@@ -257,6 +261,8 @@ let parse () =
 	Cdglobals.target_language := HTML; parse_rec rem
     | ("-texmacs" | "--texmacs") :: rem ->
 	Cdglobals.target_language := TeXmacs; parse_rec rem
+    | ("-raw" | "--raw") :: rem ->
+	Cdglobals.target_language := Raw; parse_rec rem
     | ("-charset" | "--charset") :: s :: rem ->
 	Cdglobals.charset := s; parse_rec rem
     | ("-charset" | "--charset") :: [] ->
@@ -267,6 +273,9 @@ let parse () =
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
 	Cdglobals.raw_comments := true; parse_rec rem
+    | ("-interpolate" | "--interpolate") :: rem ->
+	Cdglobals.interpolate := true; parse_rec rem
+
     | ("-latin1" | "--latin1") :: rem ->
 	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
@@ -310,6 +319,8 @@ let parse () =
 	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
+    | ("--boot" | "-boot") :: rem ->
+	Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
@@ -318,6 +329,7 @@ let parse () =
 	add_file (what_file f); parse_rec rem
   in 
     parse_rec (List.tl (Array.to_list Sys.argv));
+    Output.initialize ();
     List.rev !files
 
       
@@ -414,10 +426,10 @@ let read_glob x =
   match x with
     | Vernac_file (f,m) ->   
 	let glob = (Filename.chop_extension f) ^ ".glob" in
-	  (try
+ 	  (try
 	      Vernac_file (f, Index.read_glob glob)
-	    with _ -> 
-	      eprintf "Warning: file %s cannot be opened; links will not be available\n" glob;
+            with e -> 
+              eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
 	      x)
   | Latex_file _ -> x
 
@@ -430,13 +442,13 @@ let produce_document l =
   (if !target_language=HTML then
     let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
     let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
-      copy src dst);
+      if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
   (if !target_language=LaTeX then
       let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
       let dst = if !output_dir <> "" then 
 	  Filename.concat !output_dir "coqdoc.sty" 
 	else "coqdoc.sty" in
-	copy src dst);
+	if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
   (match !Cdglobals.glob_source with
     | NoGlob -> ()
     | DotGlob -> ignore (List.map read_glob l)
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 93414f22..c146150c 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 11154 2008-06-19 18:42:19Z msozeau $ i*)
+(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -32,43 +32,48 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint";
-      "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
+    [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+      "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
       "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
       "Module"; "Module Type"; "Declare Module"; "Include";
-      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
+      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-      "Set"; "Unset"; "Variable"; "Variables"; "Context";
+      "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; 
       "Boxed"; "Unboxed"; "Inline";
-      "Arguments"; "Add"; "Strict";
-      "Typeclasses"; "Instance"; "Class"; "Instantiation";
+      "Implicit Arguments"; "Add"; "Strict";
+      "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
+      "subgoal";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
-      "Program Instance";
+      "Program Instance"; "Equations"; "Equations_nocomp";
       (*i (* coq terms *) *)
-	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
-	"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
+      "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
+      "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      (* Ltac *)
+      "before"; "after"
        ]
 
 let is_tactic = 
   build_table
-    [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
-      "destruct"; "induction"; "elim"; "dependent"; 
-      "generalize"; "clear"; "rename"; "move"; "set"; "assert";
-      "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
+    [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
+      "elimtype"; "progress"; "setoid_rewrite";
+      "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
+      "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
+      "set"; "assert"; "do"; "repeat";
+      "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate";
       "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
-      "pattern"; "intuition"; "congruence";
+      "pattern"; "intuition"; "congruence"; "fail"; "fresh";
       "trivial"; "exact"; "tauto"; "firstorder"; "ring";
-      "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
+      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
 
 (*s Current Coq module *)
 
@@ -92,27 +97,31 @@ let find_printing_token tok =
 let remove_printing_token = Hashtbl.remove token_pp
 
 (* predefined pretty-prints *)
-let _ = List.iter 
-	  (fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
-	  [ "*" ,  "\\ensuremath{\\times}";
-	    "|", "\\ensuremath{|}";
-	    "->",  "\\ensuremath{\\rightarrow}";
-	    "->~",  "\\ensuremath{\\rightarrow\\lnot}";
-	    "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}";
-	    "<-",  "\\ensuremath{\\leftarrow}";
-	    "<->", "\\ensuremath{\\leftrightarrow}";
-	    "=>",  "\\ensuremath{\\Rightarrow}";
-	    "<=",  "\\ensuremath{\\le}";
-	    ">=",  "\\ensuremath{\\ge}";
-	    "<>",  "\\ensuremath{\\not=}";
-	    "~",   "\\ensuremath{\\lnot}";
-	    "/\\", "\\ensuremath{\\land}";
-	    "\\/", "\\ensuremath{\\lor}";
-	    "|-",  "\\ensuremath{\\vdash}";
-	    "forall", "\\ensuremath{\\forall}";
-	    "exists", "\\ensuremath{\\exists}";
-	    (* "fun", "\\ensuremath{\\lambda}" ? *)
-	  ]
+let initialize () = 
+  let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
+    List.iter 
+      (fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l'))
+      [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
+	"|", "\\ensuremath{|}", None;
+	"->",  "\\ensuremath{\\rightarrow}", if_utf8 "→";
+	"->~",  "\\ensuremath{\\rightarrow\\lnot}", None;
+	"->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}", None;
+	"<-",  "\\ensuremath{\\leftarrow}", None;
+	"<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔";
+	"=>",  "\\ensuremath{\\Rightarrow}", if_utf8 "⇒";
+	"<=",  "\\ensuremath{\\le}", if_utf8 "≤";
+	">=",  "\\ensuremath{\\ge}", if_utf8 "≥";
+	"<>",  "\\ensuremath{\\not=}", if_utf8 "≠";
+	"~",   "\\ensuremath{\\lnot}", if_utf8 "¬";
+	"/\\", "\\ensuremath{\\land}", if_utf8 "∧";
+	"\\/", "\\ensuremath{\\lor}", if_utf8 "∨";
+	"|-",  "\\ensuremath{\\vdash}", None;
+	"forall", "\\ensuremath{\\forall}", if_utf8 "∀";
+	"exists", "\\ensuremath{\\exists}", if_utf8 "∃";
+	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
+	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ"
+	(* "fun", "\\ensuremath{\\lambda}" ? *)
+      ]
 
 (*s Table of contents *)
 
@@ -130,6 +139,9 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r
 
 module Latex = struct
 
+  let in_title = ref false
+  let in_doc = ref false
+
   (*s Latex preamble *)
 
   let (preamble : string Queue.t) = Queue.create ()
@@ -208,7 +220,7 @@ module Latex = struct
 
   let indentation n = 
     if n == 0 then 
-      printf "\\noindent\n"
+      printf "\\coqdocnoindent\n"
     else
       let space = 0.5 *. (float n) in
       printf "\\coqdocindent{%2.2fem}\n" space
@@ -243,35 +255,49 @@ module Latex = struct
 	  let _m = Filename.concat !coqlib m in
 	    printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
       | Coqlib | Unknown ->
-	  raw_ident s
+	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
 
   let defref m id ty s =
     printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
 
+  let reference s = function
+    | Def (fullid,typ) -> 
+	defref !current_module 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{"; raw_ident s; printf "}"
+	  
   let ident s loc = 
     if is_keyword s then begin
       printf "\\coqdockw{"; raw_ident s; printf "}"
     end else begin
       begin
 	try
-	  (match Index.find !current_module loc with
-	     | Def (fullid,typ) -> 
-		 defref !current_module 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 "\\coqdocid{"; raw_ident s; printf "}")
+	  reference s (Index.find !current_module loc)
 	with Not_found ->
 	  if is_tactic s then begin
 	    printf "\\coqdoctac{"; raw_ident s; printf "}"
-	  end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end
+	  end else begin
+	    if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) 
+	    then
+	      try reference s (Index.find_string !current_module s)
+	      with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
+	    else (printf "\\coqdocvar{"; raw_ident s; printf "}")
+	  end
       end
     end
 
-  let ident s l = with_latex_printing (fun s -> ident s l) s
-
+  let ident s l = 
+    if !in_title then (
+      printf "\\texorpdfstring{";
+      with_latex_printing (fun s -> ident s l) s;
+      printf "}{"; raw_ident s; printf "}")
+    else
+      with_latex_printing (fun s -> ident s l) s
+    
   let symbol = with_latex_printing raw_ident
 
   let rec reach_item_level n = 
@@ -290,13 +316,13 @@ module Latex = struct
 
   let stop_item () = reach_item_level 0
 
-  let start_doc () = printf "\n\n\n\\noindent\n"
+  let start_doc () = in_doc := true
 
-  let end_doc () = stop_item (); printf "\n\n\n"
+  let end_doc () = in_doc := false; stop_item ()
 
-  let start_coq () = ()
+  let start_coq () = printf "\\begin{coqdoccode}\n"
 
-  let end_coq () = ()
+  let end_coq () = printf "\\end{coqdoccode}\n"
 
   let start_code () = end_doc (); start_coq ()
 
@@ -312,17 +338,17 @@ module Latex = struct
   let section lev f =
     stop_item ();
     output_string (section_kind lev);
-    f ();
+    in_title := true; f (); in_title := false;
     printf "}\n\n"
 
   let rule () =
     printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}"
 
-  let paragraph () = stop_item (); printf "\n\n\\medskip\n"
+  let paragraph () = stop_item (); printf "\n\n"
 
   let line_break () = printf "\\coqdoceol\n"
 
-  let empty_line_of_code () = printf "\n\n\\medskip\n"
+  let empty_line_of_code () = printf "\\coqdocemptyline\n"
 
   let start_inline_coq () = ()
 
@@ -394,7 +420,8 @@ module Html = struct
 
   let line_break () = printf "<br/>\n"
 
-  let empty_line_of_code () = printf "\n<br/>\n"
+  let empty_line_of_code () = 
+    printf "\n<br/>\n"
 
   let char = function
     | '<' -> printf "&lt;"
@@ -417,49 +444,54 @@ module Html = struct
   let stop_verbatim () = printf "</pre>\n"
 
   let module_ref m s = 
-    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    (*i
-    match find_module m with
-    | Local ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib when !externals ->
-	let m = Filename.concat !coqlib m in
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib | Unknown ->
-	raw_ident s
-    i*)
-
-  let ident_ref m fid s = 
     match find_module m with
       | Local ->
-	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+	  printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
       | Coqlib when !externals ->
 	  let m = Filename.concat !coqlib m in
-	    printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+	    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
       | Coqlib | Unknown ->
 	  raw_ident s
 
+  let ident_ref m fid typ s =
+    match find_module m with
+    | Local ->
+	printf "<span class=\"id\" type=\"%s\">" typ; 
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
+	printf "</a></span>"
+    | Coqlib when !externals ->
+	let m = Filename.concat !coqlib m in
+	  printf "<span class=\"id\" type=\"%s\">" typ; 
+	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
+	  raw_ident s; printf "</a></span>"
+    | Coqlib | Unknown ->
+	printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
+	  
   let ident s loc = 
     if is_keyword s then begin
-      printf "<span class=\"keyword\">"; 
+      printf "<span class=\"id\" type=\"keyword\">"; 
       raw_ident s; 
       printf "</span>"
     end else 
       begin
 	try
 	  (match Index.find !current_module loc with
-	     | Def (fullid,_) -> 
-		 printf "<a name=\"%s\"></a>" fullid; raw_ident s
+	     | Def (fullid,ty) -> 
+		 printf "<span class=\"id\" type=\"%s\">" (type_name ty); 
+		 printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
              | Mod (m,s') when s = s' ->
 		 module_ref m s
 	     | Ref (m,fullid,ty) -> 
-		 ident_ref m fullid s
+		 ident_ref m fullid (type_name ty) s
 	     | Mod _ ->
-		 raw_ident s)
+		 printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>")
 	with Not_found ->
-	  raw_ident s
+	  if is_tactic s then
+	    (printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
+	  else
+	    (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
       end
-	  
+
   let with_html_printing f tok =
     try 
       (match Hashtbl.find token_pp tok with
@@ -488,9 +520,9 @@ module Html = struct
 
   let stop_item () = reach_item_level 0
 
-  let start_coq () = if not !raw_comments then printf "<code>\n"
+  let start_coq () = if not !raw_comments then printf "<div class=\"code\">\n"
 
-  let end_coq () = if not !raw_comments then printf "</code>\n"
+  let end_coq () = if not !raw_comments then printf "</div>\n"
 
   let start_doc () = 
     if not !raw_comments then
@@ -504,9 +536,9 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = printf "<code>"
+  let start_inline_coq () = printf "<span class=\"inlinecode\">"
 
-  let end_inline_coq () = printf "</code>"
+  let end_inline_coq () = printf "</span>"
 
   let paragraph () = stop_item (); printf "\n<br/><br/>\n"
 
@@ -539,7 +571,7 @@ module Html = struct
   let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
 
   (* Construction d'une liste des index (1 index global, puis 1
-     index par catégorie) *)
+     index par catégorie) *)
   let format_global_index =
     Index.map 
       (fun s (m,t) -> 
@@ -578,7 +610,7 @@ module Html = struct
     printf "</table>\n"
 	
   let make_one_multi_index prt_tbl i =
-    (* Attn: make_one_multi_index créé un nouveau fichier... *)
+    (* Attn: make_one_multi_index créé un nouveau fichier... *)
     let idx = i.idx_name in
     let one_letter ((c,l) as cl) =
       open_out_file (sprintf "index_%s_%c.html" idx c);
@@ -776,68 +808,155 @@ module TeXmacs = struct
 
 end
 
+
+(*s LaTeX output *)
+
+module Raw = struct
+
+  let header () = ()
+
+  let trailer () = ()
+
+  let char = output_char
+
+  let label_char c = match c with
+    | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
+    | '^' | '~' -> ()
+    | _ -> 
+	output_char c
+
+  let latex_char = output_char
+  let latex_string = output_string
+
+  let html_char _ = ()
+  let html_string _ = ()
+
+  let raw_ident s =
+    for i = 0 to String.length s - 1 do char s.[i] done
+
+  let start_module () = ()
+  let end_module () = ()
+
+  let start_latex_math () = ()
+  let stop_latex_math () = ()
+
+  let start_verbatim () = ()
+
+  let stop_verbatim () = ()
+
+  let indentation n = 
+      for i = 1 to n do printf " " done
+
+  let ident s loc = raw_ident s
+
+  let symbol = raw_ident
+
+  let item n = printf "- "
+
+  let stop_item () = ()
+
+  let start_doc () = printf "(** "
+  let end_doc () = printf " *)\n"
+
+  let start_coq () = ()
+  let end_coq () = ()
+
+  let start_code () = end_doc (); start_coq ()
+  let end_code () = end_coq (); start_doc ()
+
+  let section_kind = 
+    function
+      | 1 -> "*"
+      | 2 -> "**"
+      | 3 -> "***"
+      | 4 -> "****"
+      | _ -> assert false    
+
+  let section lev f = 
+    output_string (section_kind lev);
+    f ()
+
+  let rule () = ()
+
+  let paragraph () = printf "\n\n"
+
+  let line_break () = printf "\n"
+
+  let empty_line_of_code () = printf "\n"
+
+  let start_inline_coq () = ()
+  let end_inline_coq () = ()
+
+  let make_multi_index () = ()
+  let make_index () = ()
+  let make_toc () = () 
+
+end
+
+
+
 (*s Generic output *)
 
-let select f1 f2 f3 x = 
-  match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x
+let select f1 f2 f3 f4 x = 
+  match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x
 
 let push_in_preamble = Latex.push_in_preamble
 
-let header = select Latex.header Html.header TeXmacs.header
-let trailer = select Latex.trailer Html.trailer TeXmacs.trailer
+let header = select Latex.header Html.header TeXmacs.header Raw.header
+let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer
 
 let start_module = 
-  select Latex.start_module Html.start_module TeXmacs.start_module
+  select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module
 
-let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc
-let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc
+let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
+let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc
 
-let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq
-let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq
+let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
+let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
 
-let start_code = select Latex.start_code Html.start_code TeXmacs.start_code
-let end_code = select Latex.end_code Html.end_code TeXmacs.end_code
+let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code
+let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code 
 
 let start_inline_coq = 
-  select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq
+  select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq
 let end_inline_coq = 
-  select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq
+  select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq
 
-let indentation = select Latex.indentation Html.indentation TeXmacs.indentation
-let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph
-let line_break = select Latex.line_break Html.line_break TeXmacs.line_break
+let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation
+let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph
+let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break
 let empty_line_of_code = select 
-  Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code
+  Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code
 
-let section = select Latex.section Html.section TeXmacs.section
-let item = select Latex.item Html.item TeXmacs.item
-let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item
-let rule = select Latex.rule Html.rule TeXmacs.rule
+let section = select Latex.section Html.section TeXmacs.section Raw.section
+let item = select Latex.item Html.item TeXmacs.item Raw.item
+let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item
+let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
-let char = select Latex.char Html.char TeXmacs.char
-let ident = select Latex.ident Html.ident TeXmacs.ident
-let symbol = select Latex.symbol Html.symbol TeXmacs.symbol
+let char = select Latex.char Html.char TeXmacs.char Raw.char
+let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
+let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol
 
-let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char
+let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char
 let latex_string = 
-  select Latex.latex_string Html.latex_string TeXmacs.latex_string
-let html_char = select Latex.html_char Html.html_char TeXmacs.html_char
+  select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string
+let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char
 let html_string = 
-  select Latex.html_string Html.html_string TeXmacs.html_string
+  select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string
 
 let start_latex_math = 
-  select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math
+  select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
 let stop_latex_math = 
-  select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math
+  select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math
 
 let start_verbatim = 
-  select Latex.start_verbatim Html.start_verbatim TeXmacs.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
+  select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
 let verbatim_char = 
-  select output_char Html.char TeXmacs.char
+  select output_char Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
-let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index
-let make_index = select Latex.make_index Html.make_index TeXmacs.make_index
-let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc
+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 87b311f3..3da80335 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 8669 2006-03-28 17:34:15Z notin $ i*)
+(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 open Cdglobals
 open Index
 
+val initialize : unit -> unit
+
 val add_printing_token : string -> string option * string option -> unit
 val remove_printing_token : string -> unit
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index baace5ba..3ae5cbed 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 11255 2008-07-24 16:57:13Z notin $ i*)
+(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -57,6 +57,7 @@
   let formatted = ref false
   let brackets = ref 0
   let comment_level = ref 0
+  let in_proof = ref false
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
@@ -173,11 +174,12 @@ let firstchar =
   ['A'-'Z' 'a'-'z' '_' 
   (* iso 8859-1 accents *) 
   '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  (* *)
   '\194' '\185' |
   (* utf-8 latin 1 supplement *) 
   '\195' ['\128'-'\191'] |
   (* utf-8 letterlike symbols *) 
-  '\206' ['\177'-'\183'] |
+  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
@@ -188,17 +190,24 @@ let pfx_id = (id '.')*
 let identifier = 
   id | pfx_id id
 
-let symbolchar_no_brackets =
-  ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'
-   '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~'
-   '{' '}' '(' ')'] |
+let symbolchar_symbol_no_brackets =
+  ['!' '$' '%' '&' '*' '+' ',' '^' '#'
+      '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
   (* utf-8 symbols *) 
   '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
+let symbolchar_no_brackets = symbolchar_symbol_no_brackets | 
+    [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
 let symbolchar = symbolchar_no_brackets | '[' | ']'
-let token_no_brackets = symbolchar_no_brackets+
-let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
+let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
+let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
 let printing_token = (token | id)+
 
+(* tokens with balanced brackets *)
+let token_brackets =
+  ( token_no_brackets ('[' token_no_brackets? ']')* 
+  | token_no_brackets? ('[' token_no_brackets? ']')+ )
+  token_no_brackets?
+
 let thm_token = 
   "Theorem" 
   | "Lemma" 
@@ -208,22 +217,26 @@ let thm_token =
   | "Proposition" 
   | "Property"
   | "Goal"
+  | "Next" space+ "Obligation"
 
 let def_token = 
   "Definition" 
   | "Let" 
   | "Class"
-  | "SubClass" 
+  | "SubClass"
   | "Example"
   | "Local" 
   | "Fixpoint" 
+  | "Boxed" 
   | "CoFixpoint" 
   | "Record" 
   | "Structure" 
-  | "Instance"
   | "Scheme"
   | "Inductive"
   | "CoInductive"
+  | "Equations"
+  | "Instance"
+  | "Global" space+ "Instance"
 
 let decl_token = 
   "Hypothesis" 
@@ -277,6 +290,8 @@ let commands =
   | ("Hypothesis" | "Hypotheses")
   | "End"
 
+let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+
 let extraction = 
   "Extraction"
   | "Recursive" space+ "Extraction" 
@@ -291,7 +306,8 @@ let prog_kw =
   | "Solve"
 
 let gallina_kw_to_hide =
-  "Implicit"
+    "Implicit" space+ "Arguments"
+  | "Next" "Obligation"
   | "Ltac"
   | "Require"
   | "Import"
@@ -308,12 +324,6 @@ let gallina_kw_to_hide =
   | "Declare" space+ ("Left" | "Right") space+ "Step" 
 
 
-(* tokens with balanced brackets *)
-let token_brackets =
-  ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* 
-  | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ )
-  symbolchar_no_brackets*
-
 let section = "*" | "**" | "***" | "****"
 
 let item_space = "    "
@@ -333,7 +343,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { Output.empty_line_of_code (); coq_bol lexbuf }
+      { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -352,7 +362,7 @@ rule coq_bol = parse
       { let s = lexeme lexbuf in
 	  if !Cdglobals.light && section_or_end s then 
 	    let eol = skip_to_dot lexbuf in
-	      if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf
+	      if eol then (coq_bol lexbuf) else coq lexbuf
 	  else 
 	    begin
 	      let nbsp,isp = count_spaces s in
@@ -362,16 +372,45 @@ rule coq_bol = parse
 		  let eol = body lexbuf in 
 		    if eol then coq_bol lexbuf else coq lexbuf
 	    end }
-  | space* gallina_kw
+  | space* thm_token
       { let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	let s = String.sub s isp (String.length s - isp)  in
 	  Output.indentation nbsp;
 	  Output.ident s (lexeme_start lexbuf + isp); 
+	  let eol = body lexbuf in
+	    in_proof := true;
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space* "Proof" (space* "." | space+ "with")
+      { in_proof := true;
+	let eol = 
+	if not !Cdglobals.gallina then 
+	  begin backtrack lexbuf; body_bol lexbuf end 
+	else true
+	in if eol then coq_bol lexbuf else coq lexbuf }
+  | space* end_kw { 
+      let eol = 
+	if not (!in_proof && !Cdglobals.gallina) then 
+	  begin backtrack lexbuf; body_bol lexbuf end 
+	else
+	  skip_to_dot lexbuf 
+      in
+	in_proof := false;
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | space* gallina_kw
+      { 
+	in_proof := false;
+	let s = lexeme lexbuf in 
+	let nbsp,isp = count_spaces s in
+	let s = String.sub s isp (String.length s - isp)  in
+	  Output.indentation nbsp;
+	  Output.ident s (lexeme_start lexbuf + isp); 
 	  let eol= body lexbuf in
 	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* prog_kw
-      { let s = lexeme lexbuf in 
+      { 
+	in_proof := false;
+	let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	  Output.indentation nbsp;
 	  let s = String.sub s isp (String.length s - isp)  in
@@ -409,7 +448,7 @@ rule coq_bol = parse
   | _
       { let eol = 
 	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end 
+	    begin backtrack lexbuf; body_bol lexbuf end 
 	  else 
 	    skip_to_dot lexbuf 
 	in
@@ -419,7 +458,7 @@ rule coq_bol = parse
 
 and coq = parse
   | nl 
-      { Output.line_break(); coq_bol lexbuf }
+      { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -448,6 +487,15 @@ and coq = parse
 	      let eol=body lexbuf in 
 		if eol then coq_bol lexbuf else coq lexbuf
 	    end }
+  | end_kw { 
+      let eol = 
+	if not (!in_proof && !Cdglobals.gallina) then 
+	  begin backtrack lexbuf; body lexbuf end 
+	else
+	  skip_to_dot lexbuf 
+      in
+	in_proof := false;
+	if eol then coq_bol lexbuf else coq lexbuf }
   | gallina_kw
       { let s = lexeme lexbuf in 
 	  Output.ident s (lexeme_start lexbuf); 
@@ -463,7 +511,7 @@ and coq = parse
       { () }
   | _ {	let eol = 
 	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; Output.indentation 0; body lexbuf end 
+	    begin backtrack lexbuf; body lexbuf end 
 	  else 
 	    let eol = skip_to_dot lexbuf in
 	      if eol then Output.line_break (); eol
@@ -496,16 +544,15 @@ and doc_bol = parse
 and doc = parse
   | nl
       { Output.char '\n'; doc_bol lexbuf }
-  | "["
-      { brackets := 1; 
-	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
-	doc lexbuf }
-  | "[[" nl space*
+  | "[[" nl
       { formatted := true; Output.line_break (); Output.start_inline_coq ();
-	Output.indentation (fst (count_spaces (lexeme lexbuf))); 
 	let eol = body_bol lexbuf in 
 	  Output.end_inline_coq (); formatted := false;
 	  if eol then doc_bol lexbuf else doc lexbuf}
+  | "["
+      { brackets := 1; 
+	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
+	doc lexbuf }
   | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
@@ -612,7 +659,7 @@ and skip_to_dot = parse
 and body_bol = parse
   | space+
       { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
-  | _ { backtrack lexbuf; body lexbuf }
+  | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
 
 and body = parse
   | nl {Output.line_break(); body_bol lexbuf}
@@ -645,7 +692,7 @@ and notation_bol = parse
 
 and notation = parse
   | nl { Output.line_break(); notation_bol lexbuf }
-  | '"' { Output.char '"'; false }
+  | '"' { Output.char '"'}
   | token
       { let s = lexeme lexbuf in
 	  Output.symbol s; notation lexbuf }
@@ -660,7 +707,7 @@ and skip_hide = parse
 (*s Reading token pretty-print *)
 
 and printing_token_body = parse
-  | "*)" | eof 
+  | "*)" nl? | eof 
 	{ let s = Buffer.contents token_buffer in 
 	  Buffer.clear token_buffer;
 	  s }