Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

24 files changed, 582 insertions, 552 deletions

diff --git a/tools/check-v8 b/tools/check-v8
deleted file mode 100755
index 9dfa0be3..00000000
--- a/tools/check-v8
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/sh
-
-echo ------------------ Producing v8 files -------------------------
-if [ -e v8 ]; then rm -r v8; fi
-if [ -e /tmp/v8.$$ ]; then rm -r /tmp/v8.$$; fi
-cp -pr . /tmp/v8.$$
-mv /tmp/v8.$$ v8
-cd v8
-rm description
-make clean
-make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
- { echo ---- Failed to translate; exit 1; }
-echo ------------------ Upgrading v8 files -------------------------
-v8files=`find . -name \*.v8`
-for i in $v8files; do
-  j=`dirname $i`/`basename $i .v8`.v
-  echo Upgrading $i
-  mv -u -f $i $j
-done
-echo ------------------ Recompiling v8 files -----------------------
-make clean
-make || { echo ---- Failed to recompile; exit 1; }
-make clean # to save disk space
-echo ------------------ Translation completed ----------------------
diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4
index 6987d78b..7565c22e 100644
--- a/tools/coq-tex.ml4
+++ b/tools/coq-tex.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq-tex.ml4,v 1.5.2.1 2004/07/16 19:31:45 herbelin Exp $ *)
+(* $Id: coq-tex.ml4 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* coq-tex
  * JCF, 16/1/98
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 02607f14..cc3e9515 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,v 1.16.2.4 2005/01/12 16:00:19 sacerdot Exp $ *)
+(* $Id: coq_makefile.ml4 7994 2006-02-06 08:48:37Z herbelin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -79,9 +79,9 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
 [--help]: equivalent to [-h]\n";
   exit 1
 
-let standard sds =
+let standard sds sps =
   print "byte:\n";
-  print "\t$(MAKE) all \"OPT=-byte\"\n\n";
+  print "\t$(MAKE) all \"OPT=\"\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";
@@ -118,6 +118,9 @@ let standard sds =
   print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n";
   print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n";
   List.iter
+    (fun (file,_,_) -> 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";
@@ -224,17 +227,16 @@ let include_dirs l =
   print "OCAMLLIBS="; print_list "\\\n  " i_ocaml; print "\n";
   print "COQLIBS=";   print_list "\\\n  " i_coq; print "\n\n"
 
-let special l =
+let rec special = function
+  | [] -> []
+  | Special (file,deps,com) :: r -> (file,deps,com) :: (special r)
+  | _ :: r -> special r
+
+let custom sps =
   let pr_sp (file,dependencies,com) =
     print file; print ": "; print dependencies; print "\n";
     print "\t"; print com; print "\n\n"
   in
-  let rec sp_aux = function
-    | [] -> []
-    | Special (file,deps,com) :: r -> (file,deps,com) :: (sp_aux r)
-    | _ :: r -> sp_aux r
-  in
-  let sps = sp_aux l in
   if sps <> [] then section "Custom targets.";
   List.iter pr_sp sps
 
@@ -434,10 +436,11 @@ let do_makefile args =
   variables l;
   include_dirs l;
   all_target l;
-  special l;
+  let sps = special  l in
+  custom sps;
   let sds = subdirs l in
   implicit ();
-  standard sds;
+  standard sds sps;
   (* TEST directories_deps l; *)
   warning ();
   if not (!output_channel == stdout) then close_out !output_channel;
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index ab7cef92..eb740712 100755..100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml,v 1.15.2.1 2004/07/16 19:31:46 herbelin Exp $ *)
+(* $Id: coqdep.ml 8642 2006-03-17 10:09:02Z notin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -523,6 +523,7 @@ let coqdep () =
   List.iter 
     (fun (s,_) -> add_coqlib_directory s)
     (all_subdirs (!coqlib/"contrib") "Coq");
+  add_coqlib_directory (!coqlib/"user-contrib");
   mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu);
   mlKnown  := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu);
   warning_mult ".mli" !mliKnown;
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 4f5f172f..f7f37086 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqdep_lexer.mll,v 1.6.6.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+(*i $Id: coqdep_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ i*)
   
 {
 
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 2418b6e1..b1a46bae 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.ml,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+(*i $Id: alpha.ml 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 let norm_char c = match Char.uppercase c with
   | '\192'..'\198' -> 'A'
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 46409c9a..d3c26537 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+(*i $Id: alpha.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Alphabetic order. *)
 
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
new file mode 100644
index 00000000..b5a4cb22
--- /dev/null
+++ b/tools/coqdoc/cdglobals.ml
@@ -0,0 +1,72 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+
+(*s Output options *)
+
+type target_language = LaTeX | HTML | TeXmacs
+
+let target_language = ref HTML
+
+type output_t =
+  | StdOut
+  | MultFiles
+  | File of string
+
+let output_dir = ref ""
+
+let out_to = ref MultFiles
+
+let out_channel = ref stdout
+
+let open_out_file f =
+  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
+    out_channel := open_out f
+
+let close_out_file () = close_out !out_channel
+
+
+let header_trailer = ref true
+let quiet = ref false
+let light = ref false
+let gallina = ref false
+let short = ref false
+let index = ref true
+let multi_index = ref false
+let toc = ref false
+let page_title = ref ""
+let title = ref ""
+let externals = ref true
+let coqlib = ref "http://coq.inria.fr/library/"
+let raw_comments = ref false
+
+let charset = ref "iso-8859-1"
+let inputenc = ref ""
+let latin1 = ref false
+let utf8 = ref false
+
+let set_latin1 () =
+  charset := "iso-8859-1";
+  inputenc := "latin1";
+  latin1 := true
+
+let set_utf8 () =
+  charset := "utf-8";
+  inputenc := "utf8";
+  utf8 := true
+
+(* Parsing options *)
+
+type coq_module = string
+
+type file =
+  | Vernac_file of string * coq_module
+  | Latex_file of string
+      
+
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
new file mode 100644
index 00000000..b59438e5
--- /dev/null
+++ b/tools/coqdoc/coqdoc.css
@@ -0,0 +1,59 @@
+body { padding: 0px 0px;
+       margin: 0px 0px; 
+       background-color: white }
+
+#page { display: block;
+        padding: 0px;
+        margin: 0px;
+        padding-bottom: 10px; }
+
+#header { display: block;
+          position: relative;
+          padding: 0;
+          margin: 0;
+          vertical-align: middle;
+          border-bottom-style: solid;
+          border-width: thin }
+
+#header h1 { padding: 0; 
+             margin: 0;}
+
+
+/* Contenu */
+
+#main{ display: block;
+       padding: 10px;
+       overflow: hidden;
+       font-size: 10pt }
+
+#main  a.idref:visited {color : #416DFF; text-decoration : none; }
+#main  a.idref:link {color : #416DFF; text-decoration : none; }
+#main  a.idref:hover {color : Red; text-decoration : underline; }
+#main  a.idref:active {color : Red; text-decoration : underline; }
+
+#main .keyword { font-weight : bold; 
+                 color : Red }
+
+#main .section { font-size : 20pt }
+
+#main code { font-family: monospace; 
+             font-size: 8pt; 
+             line-height: 50% }
+
+#main .doc { margin: 0px;
+             padding: 10px;
+             font-family: sans-serif;
+             font-size: 11pt;
+             font-weight:bold;
+             background-color:#66ff66 }
+
+#main .doc code { font-family: monospace; 
+                  font-size: 10pt} 
+
+/* Pied de page */
+
+#footer { font-size: 8pt;
+          font-family: sans-serif; }
+
+#footer a:visited { color: blue; }
+
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 68b9ab26..597152f5 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -9,13 +9,13 @@
 \ProvidesPackage{coqdoc}[2002/02/11]
 
 % Headings
-
 \usepackage{fancyhdr}
 \newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
 \newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
 \pagestyle{fancyplain}
 
 %BEGIN LATEX
+\headsep 8mm
 \renewcommand{\plainheadrulewidth}{0.4pt}
 \renewcommand{\plainfootrulewidth}{0pt}
 \lhead[\coqdocleftpageheader]{\leftmark}
@@ -50,7 +50,8 @@
 %HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}}
 
 % macro for typesetting the title of a module implementation
-\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}}
+\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}
+}
 
 %HEVEA\newcommand{\lnot}{\coqwkw{not}}
 %HEVEA\newcommand{\lor}{\coqwkw{or}}
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 60c21387..4b53d6ff 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+(*i $Id: index.mli 8617 2006-03-08 10:47:12Z notin $ i*)
 
-type coq_module = string
+open Cdglobals
 
 type loc = int
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 875a2337..ec89da2f 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mll,v 1.2.2.2 2004/08/03 17:31:04 herbelin Exp $ i*)
+(*i $Id: index.mll 8617 2006-03-08 10:47:12Z notin $ i*)
 
 {
 
@@ -14,7 +14,7 @@ open Filename
 open Lexing 
 open Printf
 
-type coq_module = string
+open Cdglobals
 
 type loc = int
 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 66d2a993..177fc2bc 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml,v 1.4.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: main.ml 8669 2006-03-28 17:34:15Z notin $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -18,6 +18,7 @@
  * It may be removed or abbreviated as far as I am concerned.
  *)
 
+open Cdglobals
 open Filename
 open Printf
 open Output
@@ -33,6 +34,7 @@ let usage () =
   prerr_endline "  --texmacs           produce a TeXmacs document";
   prerr_endline "  --dvi               output the DVI";
   prerr_endline "  --ps                output the PostScript";
+  prerr_endline "  --stdout            write output to stdout";
   prerr_endline "  -o <file>           write output in file <file>";
   prerr_endline "  -d <dir>            output files into directory <dir>";
   prerr_endline "  -g                  (gallina) skip proofs";
@@ -58,8 +60,6 @@ let usage () =
   prerr_endline "  --charset <string>  set HTML charset";
   prerr_endline "  --inputenc <string> set LaTeX input encoding";
   prerr_endline "";
-  prerr_endline 
-    "On-line documentation at http://www.lri.fr/~filliatr/coqdoc/\n";
   exit 1
 
 (*s \textbf{Banner.} Always printed. Notice that it is printed on error
@@ -71,7 +71,11 @@ let banner () =
   eprintf "This is coqdoc version %s, compiled on %s\n"
     Coq_config.version Coq_config.compile_date;
   flush stderr
-    
+
+let target_full_name f = 
+  match !target_language with
+    | HTML -> f ^ ".html"
+    | _ -> f ^ ".tex"
 
 (*s \textbf{Separation of files.} Files given on the command line are
     separated according to their type, which is determined by their
@@ -232,8 +236,10 @@ let parse () =
 	multi_index := true; parse_rec rem
     | ("-toc" | "--toc" | "--table-of-contents") :: rem ->
 	toc := true; parse_rec rem
+    | ("-stdout" | "--stdout") :: rem ->
+	out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
-	output_file := f; parse_rec rem
+	out_to := File f; parse_rec rem
     | ("-o" | "--output") :: [] -> 
 	usage ()
     | ("-d" | "--directory") :: dir :: rem ->
@@ -251,30 +257,29 @@ let parse () =
     | ("-t" | "-title" | "--title") :: [] ->
 	usage ()
     | ("-latex" | "--latex") :: rem ->
-	Output.target_language := LaTeX; parse_rec rem
+	Cdglobals.target_language := LaTeX; parse_rec rem
     | ("-dvi" | "--dvi") :: rem ->
-	Output.target_language := LaTeX; dvi := true; parse_rec rem
+	Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
     | ("-ps" | "--ps") :: rem ->
-	Output.target_language := LaTeX; ps := true; parse_rec rem
+	Cdglobals.target_language := LaTeX; ps := true; parse_rec rem
     | ("-html" | "--html") :: rem ->
-	Output.target_language := HTML; parse_rec rem
+	Cdglobals.target_language := HTML; parse_rec rem
     | ("-texmacs" | "--texmacs") :: rem ->
-	Output.target_language := TeXmacs; parse_rec rem
-
+	Cdglobals.target_language := TeXmacs; parse_rec rem
     | ("-charset" | "--charset") :: s :: rem ->
-	Output.charset := s; parse_rec rem
+	Cdglobals.charset := s; parse_rec rem
     | ("-charset" | "--charset") :: [] ->
 	usage ()
     | ("-inputenc" | "--inputenc") :: s :: rem ->
-	Output.inputenc := s; parse_rec rem
+	Cdglobals.inputenc := s; parse_rec rem
     | ("-inputenc" | "--inputenc") :: [] ->
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
-	Output.raw_comments := true; parse_rec rem
+	Cdglobals.raw_comments := true; parse_rec rem
     | ("-latin1" | "--latin1") :: rem ->
-	Output.set_latin1 (); parse_rec rem
+	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
-	Output.set_utf8 (); parse_rec rem
+	Cdglobals.set_utf8 (); parse_rec rem
 
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
@@ -298,7 +303,6 @@ let parse () =
 	parse_rec rem
     | ("-files" | "--files") :: [] ->
 	usage ()
-
     | "-R" :: path :: log :: rem -> 
 	add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
@@ -308,12 +312,11 @@ let parse () =
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
-	Output.externals := false; parse_rec rem
+	Cdglobals.externals := false; parse_rec rem
     | ("--coqlib" | "-coqlib") :: u :: rem ->
-	Output.coqlib := u; parse_rec rem
+	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
-
     | f :: rem -> 
 	add_file (what_file f); parse_rec rem
   in 
@@ -360,52 +363,128 @@ let copy src dst =
   with End_of_file ->
     close_in cin; close_out cout
 
+
+(*s Functions for generating output files *)
+
+let gen_one_file l =
+  let file = function
+    | Vernac_file (f,m) -> 
+	set_module m; coq_file f m
+    | Latex_file _ -> ()
+  in
+    if (!header_trailer) then header ();
+    if !toc then make_toc ();
+    List.iter file l;
+    if !index then make_index();
+    if (!header_trailer) then trailer ()
+      
+let gen_mult_files l =
+  let file = function
+    | Vernac_file (f,m) -> 
+	set_module m;
+	let hf = target_full_name m in
+	  open_out_file hf;
+	  if (!header_trailer) then header (); 
+	  if !toc then make_toc ();
+	  coq_file f m; 
+	  if (!header_trailer) then trailer ();
+	  close_out_file()
+    | Latex_file _ -> ()
+  in
+    List.iter file l;
+    if (!index && !target_language=HTML) then begin
+      if (!multi_index) then make_multi_index (); 
+      open_out_file "index.html"; 
+      page_title := (if !title <> "" then !title else "Index");
+      if (!header_trailer) then header (); 
+      make_index (); 
+      if (!header_trailer) then trailer ();
+      close_out_file()
+    end;
+    if (!toc && !target_language=HTML) then begin
+      open_out_file "toc.html"; 
+      page_title := (if !title <> "" then !title else "Table of contents");
+      if (!header_trailer) then header ();
+      if !title <> "" then printf "<h1>%s</h1>\n" !title;
+      make_toc (); 
+      if (!header_trailer) then trailer ();
+      close_out_file()
+    end 
+      (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
+
+
+let index_module = function
+  | Vernac_file (_,m) -> Index.add_module m
+  | Latex_file _ -> ()
+
+let produce_document l =
+  List.iter index_module l;
+  (if !target_language=HTML then
+    let src = (Filename.concat Coq_config.coqlib "/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 !target_language=LaTeX then
+    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in
+    let dst = if !output_dir <> "" then 
+      Filename.concat !output_dir "coqdoc.sty" 
+    else "coqdoc.sty" in
+      copy src dst);
+  match !out_to with
+    | StdOut -> 
+	Cdglobals.out_channel := stdout;
+	gen_one_file l
+    | File f ->
+	open_out_file f;
+	gen_one_file l;
+	close_out_file()
+    | MultFiles ->
+	gen_mult_files l
+
 let produce_output fl =
   if not (!dvi || !ps) then begin
-    if !output_file <> "" then set_out_file !output_file;
     produce_document fl
   end else begin
     let texfile = temp_file "coqdoc" ".tex" in
     let basefile = chop_suffix texfile ".tex" in
-    set_out_file texfile;
-    produce_document fl;
-    let command = 
-      let file = basename texfile in
-      let file = 
-	if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
-      in
-      sprintf "(latex %s && latex %s) 1>&2 %s" file file
-	(if !quiet then "> /dev/null" else "")
-    in
-    let res = locally (dirname texfile) Sys.command command in
-    if res <> 0 then begin
-      eprintf "Couldn't run LaTeX successfully\n"; 
-      clean_and_exit basefile res
-    end;
-    let dvifile = basefile ^ ".dvi" in
-    if !dvi then begin
-      if !output_file <> "" then 
-	(* we cannot use Sys.rename accross file systems *)
-	copy dvifile !output_file 
-      else 
-	cat dvifile
-    end;
-    if !ps then begin
-      let psfile = 
-	if !output_file <> "" then !output_file else basefile ^ ".ps" 
-      in
+      open_out_file texfile;
+      produce_document fl;
       let command = 
-	sprintf "dvips %s -o %s %s" dvifile psfile 
-	  (if !quiet then "> /dev/null 2>&1" else "")
+	let file = basename texfile in
+	let file = 
+	  if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+	in
+	  sprintf "(latex %s && latex %s) 1>&2 %s" file file
+	    (if !quiet then "> /dev/null" else "")
       in
-      let res = Sys.command command in
-      if res <> 0 then begin
-	eprintf "Couldn't run dvips successfully\n"; 
-	clean_and_exit basefile res
-      end;
-      if !output_file = "" then cat psfile
-    end;
-    clean_temp_files basefile
+      let res = locally (dirname texfile) Sys.command command in
+	if res <> 0 then begin
+	  eprintf "Couldn't run LaTeX successfully\n"; 
+	  clean_and_exit basefile res
+	end;
+	let dvifile = basefile ^ ".dvi" in
+	  if !dvi then begin
+	    if !output_file <> "" then 
+	      (* we cannot use Sys.rename accross file systems *)
+	      copy dvifile !output_file 
+	    else 
+	      cat dvifile
+	  end;
+	  if !ps then begin
+	    let psfile = 
+	      if !output_file <> "" then !output_file else basefile ^ ".ps" 
+	    in
+	    let command = 
+	      sprintf "dvips %s -o %s %s" dvifile psfile 
+		(if !quiet then "> /dev/null 2>&1" else "")
+	    in
+	    let res = Sys.command command in
+	      if res <> 0 then begin
+		eprintf "Couldn't run dvips successfully\n"; 
+		clean_and_exit basefile res
+	      end;
+	      if !output_file = "" then cat psfile
+	  end;
+	  clean_temp_files basefile
   end
 
 
@@ -415,6 +494,6 @@ let produce_output fl =
 let main () =
   let files = parse () in
   if not !quiet then banner ();
-  if List.length files > 0 then produce_output files
+  if files <> [] then produce_output files
 
 let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index c10f3683..4c4cf5ec 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -6,30 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: output.ml 8669 2006-03-28 17:34:15Z notin $ i*)
 
+open Cdglobals
 open Index
 
-(*s Target language *)
-
-type target_language = LaTeX | HTML | TeXmacs
-
-let target_language = ref HTML
-
 (*s Low level output *)
 
-let out_channel = ref stdout
-let output_is_file = ref false
-let output_dir = ref ""
-
-let set_out_file f = 
-  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
-  out_channel := open_out f;
-  output_is_file := true
-
-let close () =
-  if !output_is_file then close_out !out_channel
-
 let output_char c = Pervasives.output_char !out_channel c
 
 let output_string s = Pervasives.output_string !out_channel s
@@ -38,43 +21,6 @@ let printf s = Printf.fprintf !out_channel s
 
 let sprintf = Printf.sprintf
 
-let dump_file f =
-  let ch = open_in f in
-  try
-    while true do
-      Pervasives.output_char !out_channel (input_char ch)
-    done
-  with End_of_file -> close_in ch
-
-(*s Options *)
-
-let header_trailer = ref true
-let quiet = ref false
-let light = ref false
-let short = ref false
-let index = ref true
-let multi_index = ref false
-let toc = ref false
-let page_title = ref ""
-let title = ref ""
-let externals = ref true
-let coqlib = ref "http://coq.inria.fr/library/"
-let raw_comments = ref false
-
-let charset = ref ""
-let inputenc = ref ""
-let latin1 = ref false
-let utf8 = ref false
-
-let set_latin1 () =
-  charset := "iso-8859-1";
-  inputenc := "latin1";
-  latin1 := true
-
-let set_utf8 () =
-  charset := "utf-8";
-  inputenc := "utf8";
-  utf8 := true
 
 (*s Coq keywords *)
 
@@ -85,9 +31,9 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
+    [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
       "CoInductive"; "Defined"; "Definition"; 
-      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
+      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
       "Immediate"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
@@ -145,6 +91,7 @@ let _ = List.iter
 	    "|-",  "\\ensuremath{\\vdash}";
 	    "forall", "\\ensuremath{\\forall}";
 	    "exists", "\\ensuremath{\\exists}";
+	    (* "fun", "\\ensuremath{\\lambda}" ? *)
 	  ]
 
 (*s Table of contents *)
@@ -308,6 +255,8 @@ module Latex = struct
 
   let end_inline_coq () = ()
 
+  let make_multi_index () = ()
+
   let make_index () = ()
 
   let make_toc () = printf "\\tableofcontents\n"
@@ -321,29 +270,31 @@ module Html = struct
 
   let header () =
     if !header_trailer then begin
+      printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
+      printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
       printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
-      if !charset != "" then 
-	printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\">" !charset;
-      printf "<link rel=\"stylesheet\" href=\"style.css\" type=\"text/css\">";
+      printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
+      printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
       printf "<title>%s</title>\n</head>\n\n" !page_title;
-      printf "<body>\n\n"
+      printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
+      printf "<div id=\"main\">\n\n"
     end
 
-  let self = "http://www.lri.fr/~filliatr/coqdoc/"
+  let self = "http://coq.inria.fr"
 
   let trailer () =
     if !index && !current_module <> "Index" then 
-      printf "<hr/><a href=\"index.html\">Index</a>";
+      printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
     if !header_trailer then begin
       printf "<hr/><font size=\"-1\">This page has been generated by ";
       printf "<a href=\"%s\">coqdoc</a></font>\n" self;
-      printf "</body>\n</html>"
+      printf "</div>\n\n</div>\n\n</body>\n</html>"
     end
 
   let start_module () = 
     if not !short then begin
       (* add_toc_entry (Toc_library !current_module); *)
-      printf "<h1>Library %s</h1>\n\n" !current_module
+      printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
     end
 
   let indentation n = for i = 1 to n do printf "&nbsp;" done
@@ -373,7 +324,7 @@ module Html = struct
   let stop_verbatim () = printf "</pre>\n"
 
   let module_ref m s = 
-    printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
     (*i
     match find_module m with
     | Local ->
@@ -387,18 +338,18 @@ module Html = struct
 
   let ident_ref m s = match find_module m with
     | Local ->
-	printf "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
     | Coqlib when !externals ->
 	let m = Filename.concat !coqlib m in
-	printf "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
     | Coqlib | Unknown ->
 	raw_ident s
 
   let ident s loc = 
     if is_keyword s then begin
-      printf "<code class=\"keyword\">"; 
+      printf "<span class=\"keyword\">"; 
       raw_ident s; 
-      printf "</code>"
+      printf "</span>"
     end else 
       try
 	(match Index.find !current_module loc with
@@ -447,11 +398,11 @@ module Html = struct
 
   let start_doc () = 
     if not !raw_comments then
-      printf "\n<table width=\"100%%\"><tr class=\"doc\"><td>\n"
+      printf "\n<div class=\"doc\">\n"
 
   let end_doc () =
     stop_item (); 
-    if not !raw_comments then printf "\n</td></tr></table>\n"
+    if not !raw_comments then printf "\n</div>\n"
 
   let start_code () = end_doc (); start_coq ()
 
@@ -470,7 +421,7 @@ module Html = struct
     stop_item ();
     printf "<a name=\"%s\"></a><h%d>" lab lev;
     f ();
-    printf "</h%d>\n" lev
+    printf "</h%d class=\"section\">\n" lev
 
   let rule () = printf "<hr/>\n"
 
@@ -502,20 +453,8 @@ module Html = struct
 		
   let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
 
-  let separate_index navig i =
-    let idx = i.idx_name in
-    let one_letter ((c,l) as cl) =
-      set_out_file (sprintf "index_%s_%c.html" idx c);
-      header ();
-      navig ();
-      printf "<hr/>";
-      letter_index true idx cl;
-      if List.length l > 30 then begin printf "<hr/>"; navig () end;
-      trailer ();
-      close ()
-    in
-    List.iter one_letter i.idx_entries
-
+  (* Construction d'une liste des index (1 index global, puis 1
+     index par catégorie) *)
   let format_global_index =
     Index.map 
       (fun s (m,t) -> 
@@ -523,7 +462,7 @@ module Html = struct
 	   "[library]", m ^ ".html"
 	 else
 	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m ,
-	   sprintf "%s.html#%s" m s)
+	 sprintf "%s.html#%s" m s)
 
   let format_bytype_index = function
     | Library, idx ->
@@ -532,9 +471,10 @@ module Html = struct
 	Index.map 
 	  (fun s m -> 
 	     let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
-	     (text, sprintf "%s.html#%s" m s)) idx
+	       (text, sprintf "%s.html#%s" m s)) idx
 
-  let navig_one_index i =
+  (* Impression de la table d'index *)
+  let print_index_table_item i =
     printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
     List.iter 
       (fun (c,l) -> 
@@ -544,52 +484,58 @@ module Html = struct
 	   printf "<td>%c</td>\n" c)
       i.idx_entries;
     let n = i.idx_size in
-    printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
-    printf "</tr>\n"
+      printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
+      printf "</tr>\n"
 
-  let navig_index il = 
+  let print_index_table idxl = 
     printf "<table>\n";
-    List.iter navig_one_index il;
+    List.iter print_index_table_item idxl;
     printf "</table>\n"
-
+	
+  let make_one_multi_index prt_tbl i =
+    (* 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);
+      if (!header_trailer) then header ();
+      prt_tbl (); printf "<hr/>";
+      letter_index true idx cl;
+      if List.length l > 30 then begin printf "<hr/>"; prt_tbl () end;
+      if (!header_trailer) then trailer ();
+      close_out_file ()
+    in
+      List.iter one_letter i.idx_entries
+
+  let make_multi_index () = 
+    let all_index = 
+      let glob,bt = Index.all_entries () in
+	(format_global_index glob) ::
+	  (List.map format_bytype_index bt) in
+    let print_table () = print_index_table all_index in
+      List.iter (make_one_multi_index print_table) all_index
+	
   let make_index () =
-    if !index then begin
-      let idxl = 
-	let glob,bt = Index.all_entries () in
-	format_global_index glob ::
-	List.map format_bytype_index bt 
-      in
-      let navig () = navig_index idxl in 
-      set_out_file "index.html";
+    let all_index = 
+      let glob,bt = Index.all_entries () in
+	(format_global_index glob) ::
+	  (List.map format_bytype_index bt) in
+    let print_table () = print_index_table all_index in
+    let print_one_index i =
+      if i.idx_size > 0 then begin
+	printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
+	all_letters i
+      end
+    in
       current_module := "Index";
-      page_title := (if !title <> "" then !title else "Index");
-      header ();
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
-      navig ();
-      if !multi_index then begin
-	trailer (); 
-	close ();
-	List.iter (separate_index navig) idxl;
-      end else begin
-	let one_index i =
-	  if i.idx_size > 0 then begin
-	    printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
-	    all_letters i
-	  end
-	in
-	List.iter one_index idxl;
-	printf "<hr/>";
-	navig ();
-	trailer ();
-	close ()
-      end;
-    end
-
+      print_table ();
+      if not (!multi_index) then 
+	begin
+	  List.iter print_one_index all_index;
+	  printf "<hr/>"; print_table ()
+	end
+	    
   let make_toc () = 
-    set_out_file "toc.html";
-    page_title := (if !title <> "" then !title else "Table of contents");
-    header ();
-    if !title <> "" then printf "<h1>%s</h1>\n" !title;
     let make_toc_entry = function
       | Toc_library m -> 
 	  stop_item ();
@@ -600,9 +546,6 @@ module Html = struct
     in
     Queue.iter make_toc_entry toc_q;
     stop_item ();
-    if !index then printf "<a href=\"index.html\"><h2>Index</h2></a>";
-    trailer ();
-    close ()
 
 end
 
@@ -740,6 +683,8 @@ module TeXmacs = struct
 
   let end_inline_coq () = printf "]>"
 
+  let make_multi_index () = ()
+
   let make_index () = ()
 
   let make_toc () = ()
@@ -808,5 +753,6 @@ let verbatim_char =
   select output_char Html.char TeXmacs.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
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 2195fa53..87b311f3 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,35 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli,v 1.3.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: output.mli 8669 2006-03-28 17:34:15Z notin $ i*)
 
+open Cdglobals
 open Index
 
-type target_language = LaTeX | HTML | TeXmacs
-
-val target_language : target_language ref
-
-val set_out_file : string -> unit
-val output_dir : string ref
-val close : unit -> unit
-
-val quiet : bool ref
-val short : bool ref
-val light : bool ref
-val header_trailer : bool ref
-val index : bool ref
-val multi_index : bool ref
-val toc : bool ref
-val title : string ref
-val externals : bool ref
-val coqlib : string ref
-val raw_comments : bool ref
-
-val charset : string ref
-val inputenc : string ref
-val set_latin1 : unit -> unit
-val set_utf8 : unit -> unit
-
 val add_printing_token : string -> string option * string option -> unit
 val remove_printing_token : string -> unit
 
@@ -45,8 +21,6 @@ val trailer : unit -> unit
 
 val push_in_preamble : string -> unit
 
-val dump_file : string -> unit
-
 val start_module : unit -> unit
 
 val start_doc : unit -> unit
@@ -88,5 +62,6 @@ val stop_latex_math : unit -> unit
 val start_verbatim : unit -> unit
 val stop_verbatim : unit -> unit
 
+val make_multi_index : unit -> unit
 val make_index : unit -> unit
 val make_toc : unit -> unit
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli
index 07808fe9..dda0439e 100644
--- a/tools/coqdoc/pretty.mli
+++ b/tools/coqdoc/pretty.mli
@@ -6,14 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mli,v 1.1.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: pretty.mli 8617 2006-03-08 10:47:12Z notin $ i*)
 
 open Index
 
-type file =
-  | Vernac_file of string * coq_module
-  | Latex_file of string
-
-val gallina : bool ref
-
-val produce_document : file list -> unit
+val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 541939b5..ad9057ad 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: pretty.mll 8666 2006-03-27 17:02:49Z notin $ i*)
 
 (*s Utility functions for the scanners *)
 
 {
 
+  open Cdglobals
   open Printf
   open Index
   open Lexing 
@@ -56,39 +57,8 @@
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
-  (* Gallina (skipping proofs). This is a three states automaton. *)   
-
-  let gallina = ref false
-
-  type gallina_state = Nothing | AfterDot | Proof
-
-  let gstate = ref AfterDot
-
-  let is_proof = 
-    let t = Hashtbl.create 13 in
-    List.iter (fun s -> Hashtbl.add t s true)
-      [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let";
-	"Correctness"; "Definition"; "Morphism" ];
-    fun s -> try Hashtbl.find t s with Not_found -> false
-
-  let gallina_id id = 
-    if !gstate = AfterDot then
-      if is_proof id then gstate := Proof else 
-	if id <> "Add" then gstate := Nothing
-
-  let gallina_symbol s = 
-    if !gstate = AfterDot || (!gstate = Proof && s = ":=") then 
-      gstate := Nothing
-
   let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
 
-  let gallina_char c = 
-    if c = '.' then
-      (let skip = !gstate = Proof in gstate := AfterDot; skip)
-    else
-      (if !gstate = AfterDot && not (is_space c) then gstate := Nothing;
-       false)
-
   (* saving/restoring the PP state *)
 
   type state = {
@@ -121,8 +91,7 @@
 
   let reset () =
     formatted := false;
-    brackets := 0;
-    gstate := AfterDot
+    brackets := 0
 
   (* erasing of Section/End *)
 
@@ -216,6 +185,100 @@ let symbolchar_no_brackets =
 let symbolchar = symbolchar_no_brackets | '[' | ']'
 let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
 
+
+let thm_token = 
+  "Theorem" 
+  | "Lemma" 
+  | "Fact" 
+  | "Remark" 
+  | "Corollary" 
+  | "Proposition" 
+  | "Property"
+  | "Goal"
+
+let def_token = 
+  "Definition" 
+  | "Let" 
+  | "SubClass" 
+  | "Example"
+  | "Local" 
+  | "Fixpoint" 
+  | "CoFixpoint" 
+  | "Record" 
+  | "Structure" 
+  | "Scheme"
+  | "Inductive"
+  | "CoInductive"
+
+let decl_token = 
+  "Hypothesis" 
+  | "Hypotheses" 
+  | "Parameter" 
+  | "Axiom" 's'? 
+  | "Conjecture"
+
+let gallina_ext =
+  "Module" 
+  | "Declare"
+  | "Transparent"
+  | "Opaque"
+  | "Canonical"
+  | "Coercion"
+  | "Identity"
+  | "Implicit"
+  | "Notation"
+  | "Infix"
+  | "Tactic" space+ "Notation"
+  | "Reserved" space+ "Notation"
+
+let commands = 
+  "Pwd"
+  | "Cd"
+  | "Drop"
+  | "ProtectedLoop"
+  | "Quit"
+  | "Load"
+  | "Add"
+  | "Remove" space+ "Loadpath"
+  | "Print"
+  | "Inspect"
+  | "About"
+  | "Search"
+  | "Eval"
+  | "Reset"
+  | "Check"
+  | "Type"
+
+let extraction = 
+  "Extraction"
+  | "Recursive" space+ "Extraction" 
+  | "Extract"
+
+let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
+
+let gallina_kw_to_hide =
+  "Implicit"
+  | "Ltac"
+  | "Require"
+  | "Import"
+  | "Export"
+  | "Load" 
+  | "Hint"
+  | "Open"
+  | "Close"
+  | "Delimit"
+  | "Transparent"
+  | "Opaque"
+  | ("Declare" space+ ("Morphism" | "Step") )
+  | "Section"
+  | "Chapter"
+  | "Variable" 's'?
+  | ("Hypothesis" | "Hypotheses")
+  | "End"
+  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | "Declare" space+ ("Left" | "Right") space+ "Step" 
+
+
 (* tokens with balanced brackets *)
 let token_brackets =
   ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* 
@@ -235,32 +298,18 @@ let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
 let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 *)
 
-let coq_command_to_hide =
-  "Implicit" space |
-  "Ltac" space | 
-  "Require" space | 
-  "Load" space |
-  "Hint" space |
-  "Transparent" space |
-  "Opaque" space |
-  ("Declare" space+ ("Morphism" | "Step") space) |
-  "Section" space | 
-  "Variable" 's'? space | 
-  ("Hypothesis" | "Hypotheses") space | 
-  "End" space |
-  ("Set" | "Unset") space+ "Printing" space+ "Coercions" space |
-  "Declare" space+ ("Left" | "Right") space+ "Step" space
+
 
 (*s Scanning Coq, at beginning of line *)
 
 rule coq_bol = parse
-  | '\n'+
+  | space* '\n'+
       { empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { end_coq (); start_doc (); 
 	let eol = doc_bol lexbuf in
-	end_doc (); start_coq (); 
-	if eol then coq_bol lexbuf else coq lexbuf }
+	  end_doc (); start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | space* "Comments" space_nl
       { end_coq (); start_doc (); comments lexbuf; end_doc (); 
 	start_coq (); coq lexbuf }
@@ -270,28 +319,40 @@ rule coq_bol = parse
       { begin_show (); coq_bol lexbuf }
   | space* end_show
       { end_show (); coq_bol lexbuf }
-  | space* coq_command_to_hide
+  | space* gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	if !light && section_or_end s then begin 
-	  skip_to_dot lexbuf; 
-	  coq_bol lexbuf 
-	end else begin
-	  indentation (count_spaces s); 
-	  backtrack lexbuf; 
-	  coq lexbuf 
-	end }
+	  if !light && section_or_end s then begin 
+	    skip_to_dot lexbuf; 
+	    coq_bol lexbuf 
+	  end else begin
+	    let s = lexeme lexbuf in 
+	    let nbsp = count_spaces s in
+	      indentation nbsp; 
+	      let s = String.sub s nbsp (String.length s - nbsp) in
+		ident s (lexeme_start lexbuf + nbsp); 
+		let eol= body lexbuf in 
+		  if eol then coq_bol lexbuf else coq lexbuf
+	  end }
+  | space* gallina_kw
+      { let s = lexeme lexbuf in 
+	let nbsp = count_spaces s in
+	  indentation nbsp;
+	  let s = String.sub s nbsp (String.length s - nbsp)  in
+	    ident s (lexeme_start lexbuf + nbsp); 
+	    let eol= body lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf }
   | space* "(**" space+ "printing" space+ (identifier | token) space+
       { let tok = lexeme lexbuf in
 	let s = printing_token lexbuf in
-	add_printing_token tok s;
-	coq_bol lexbuf }
+	  add_printing_token tok s;
+	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
       { eprintf "warning: bad 'printing' command at character %d\n" 
 	  (lexeme_start lexbuf); flush stderr;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+ 
-    (identifier | token) space* "*)"
+      (identifier | token) space* "*)"
       { remove_printing_token (lexeme lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+
@@ -301,68 +362,77 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { let eol = comment lexbuf in
-	if eol then coq_bol lexbuf else coq lexbuf }
-  | space+
-      { indentation (count_spaces (lexeme lexbuf)); coq lexbuf }
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
       { () }
-  | _ 
-      { backtrack lexbuf; indentation 0; coq lexbuf }
+  | _
+      { let eol = 
+	  if not !gallina then 
+	    begin backtrack lexbuf; indentation 0; body_bol lexbuf end 
+	  else 
+	    skip_to_dot lexbuf 
+	in
+	  if eol then coq_bol lexbuf else coq lexbuf }
 
 (*s Scanning Coq elsewhere *)
 
 and coq = parse
   | "\n" 
-      { line_break (); coq_bol lexbuf }
+      { line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { end_coq (); start_doc (); 
 	let eol = doc_bol lexbuf in
-	end_doc (); start_coq (); 
-	if eol then coq_bol lexbuf else coq lexbuf }
+	  end_doc (); start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
       { let eol = comment lexbuf in
-	if eol then coq_bol lexbuf else coq lexbuf }
+	  if eol then begin line_break(); coq_bol lexbuf end 
+          else coq lexbuf
+      }
   | '\n'+ space* "]]"
       { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
-  | token
+  | gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	if !gallina then gallina_symbol s;
-	symbol s;
-	coq lexbuf }
-  | "with" space+ "Module" | "Module" space+ "Type" | "Declare" space+ "Module"
-    (* hack to avoid making Type a keyword *)
-      { let s = lexeme lexbuf in
-	if !gallina then gallina_id s;
-        ident s (lexeme_start lexbuf); coq lexbuf }
-  | "(" space* identifier space* ":=" 
-      { let id = extract_ident (lexeme lexbuf) in
-	symbol "("; ident id (lexeme_start lexbuf); symbol ":="; coq lexbuf }
-  | (identifier '.')* identifier
-      { let id = lexeme lexbuf in
-	if !gallina then gallina_id id;
-	ident id (lexeme_start lexbuf); coq lexbuf }
-  | _ 
-      { let c = lexeme_char lexbuf 0 in 
-	char c;
-	if !gallina && gallina_char c then skip_proof lexbuf;
-	coq lexbuf }
-
+	  if !light && section_or_end s then begin 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf 
+	  end else begin
+	    ident s (lexeme_start lexbuf); 
+	    let eol=body lexbuf in 
+	      if eol then coq_bol lexbuf else coq lexbuf
+	  end }
+  | gallina_kw
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); 
+	  let eol = body lexbuf in
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space+ { char ' '; coq lexbuf }
+  | eof 
+      { () }
+  | _ { let eol = 
+	  if not !gallina then 
+	    begin backtrack lexbuf; indentation 0; body lexbuf end 
+	  else 
+	    skip_to_dot lexbuf 
+	in 
+	  if eol then coq_bol lexbuf else coq lexbuf}
+      
 (*s Scanning documentation, at beginning of line *)
-
+      
 and doc_bol = parse
   | space* "\n" '\n'*
       { paragraph (); doc_bol lexbuf }
   | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])*
-      { let lev, s = sec_title (lexeme lexbuf) in 
-	section lev (fun () -> ignore (doc (from_string s))); 
-	doc lexbuf }
-  | space* '-'+
-      { let n = count_dashes (lexeme lexbuf) in
-	if n >= 4 then rule () else item n;
-	doc lexbuf }
-  | "<<" space*
+{ let lev, s = sec_title (lexeme lexbuf) in 
+    section lev (fun () -> ignore (doc (from_string s))); 
+    doc lexbuf }
+| space* '-'+
+     { let n = count_dashes (lexeme lexbuf) in
+	 if n >= 4 then rule () else item n;
+	 doc lexbuf }
+| "<<" space*
       { start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
   | eof 
       { false }
@@ -481,22 +551,33 @@ and comment = parse
   | eof  { false }
   | _    { comment lexbuf }
 
-(*s Skip proofs *)
-
-and skip_proof = parse
-  | "(*" { ignore (comment lexbuf); skip_proof lexbuf }
-  | "Save" | "Qed" | "Defined"
-  | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf }
-  | "Proof" space* '.' { skip_proof lexbuf }
-  | identifier { skip_proof lexbuf } (* to avoid keywords within idents *)
-  | eof { () }
-  | _ { skip_proof lexbuf }
-
 and skip_to_dot = parse
-  | eof | '.' { if !gallina then gstate := AfterDot }
+  | '.' space* '\n' { true }
+  | eof | '.' space+ { false}
   | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
+and body_bol = parse
+  | space+
+      { indentation (count_spaces (lexeme lexbuf)); body lexbuf }
+  | _ { backtrack lexbuf; body lexbuf }
+
+and body = parse
+  | '\n' {line_break(); body_bol lexbuf}
+  | eof { false }
+  | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }      
+  | '.' space+ { char '.'; char ' '; false }
+  | "(*" { let eol = comment lexbuf in 
+	     if eol then body_bol lexbuf else body lexbuf }
+  | identifier 
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); body lexbuf }
+  | token
+      { let s = lexeme lexbuf in
+	  symbol s; body lexbuf }
+  | _ { let c = lexeme_char lexbuf 0 in 
+	  char c; body lexbuf }
+
 and skip_hide = parse
   | eof | end_hide { () }
   | _ { skip_hide lexbuf }
@@ -515,10 +596,6 @@ and printing_token = parse
 
 {
 
-  type file =
-    | Vernac_file of string * coq_module
-    | Latex_file of string
-
   let coq_file f m =
     reset ();
     Index.scan_file f m;
@@ -528,59 +605,5 @@ and printing_token = parse
     start_coq (); coq_bol lb; end_coq ();
     close_in c
 
-  (* LaTeX document *)
-
-  let latex_document l = 
-    let file = function
-      | Vernac_file (f,m) -> set_module m; coq_file f m
-      | Latex_file f -> dump_file f
-    in
-    header ();
-    if !toc then make_toc ();
-    List.iter file l;
-    trailer ();
-    close ()
-
-  (* HTML document *)      
-
-  let html_document l =
-    let file = function
-      | Vernac_file (f,m) -> 
-	  set_module m;
-	  let hf = m ^ ".html" in
-	  set_out_file hf;
-	  header ();
-	  coq_file f m;
-	  trailer ();
-	  close ()
-      | Latex_file _ -> ()
-    in
-    List.iter file l;
-    make_index ();
-    if !toc then make_toc ()
-
-  (* TeXmacs document *)
-
-  let texmacs_document l = 
-    let file = function
-      | Vernac_file (f,m) -> set_module m; coq_file f m
-      | Latex_file f -> dump_file f
-    in
-    header ();
-    List.iter file l;
-    trailer ();
-    close ()
-
-  let index_module = function
-    | Vernac_file (_,m) -> Index.add_module m
-    | Latex_file _ -> ()
-
-  let produce_document l =
-    List.iter index_module l;
-    (match !target_language with
-       | LaTeX -> latex_document 
-       | HTML -> html_document
-       | TeXmacs -> texmacs_document) l
-
 }
 
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 08bf2bcc..26b64095 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -9,7 +9,7 @@
 (* coqwc - counts the lines of spec, proof and comments in Coq sources
  * Copyright (C) 2003 Jean-Christophe Filliâtre *)
 
-(*i $Id: coqwc.mll,v 1.2.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+(*i $Id: coqwc.mll 7095 2005-05-31 15:05:23Z filliatr $ 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. *)
@@ -99,7 +99,7 @@ let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
 let proof_start =   
   "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness"
 let proof_end =
-  ("Save" | "Qed" | "Defined" | "Abort") [^'.']* '.'
+  ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.'
 
 (*s [spec] scans the specification. *)
 
diff --git a/tools/gallina.ml b/tools/gallina.ml
index c997820c..a2c05c6d 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gallina.ml,v 1.2.16.1 2004/07/16 19:31:46 herbelin Exp $ *)
+(* $Id: gallina.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Gallina_lexer
 
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index ce9fb950..0b769dbd 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gallina_lexer.mll,v 1.5.6.1 2004/07/16 19:31:46 herbelin Exp $ *)
+(* $Id: gallina_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 {
  open Lexing
diff --git a/tools/restore-v7 b/tools/restore-v7
deleted file mode 100755
index ab884587..00000000
--- a/tools/restore-v7
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/sh
-
-echo Restoring v7 files from directory v7
-v7files=`find v7 -name \*.v`
-for i in $v7files; do
-  j=`echo $i | sed -e "s@^v7/@@"`
-  echo Restoring $i from v7
-  cp -f $i $j
-done
diff --git a/tools/translate-v8 b/tools/translate-v8
deleted file mode 100755
index 7d71bea9..00000000
--- a/tools/translate-v8
+++ /dev/null
@@ -1,41 +0,0 @@
-#!/bin/sh
-
-if [ -e v7 ]; then
-  echo "Warning: v7 directory found, the files are maybe already translated";
-  sleep 5;
-fi
-echo --------- Producing v8 files in the translation directory -------------
-if [ -e v8 ]; then rm -r v8; fi
-if [ -e /tmp/v7.$$ ]; then rm -r /tmp/v7.$$; fi
-cp -pr . /tmp/v7.$$
-cp -pr /tmp/v7.$$ v8
-cd v8
-rm description toto
-make clean
-make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
- { echo ---- Failed to translate; exit 1; }
-echo --------- Upgrading files in the translation directory ----------------
-v8files=`find . -name \*.v8`
-for i in $v8files; do
-  j=`dirname $i`/`basename $i .v8`.v
-  echo Upgrading $j in the translation directory
-  mv -u -f $i $j
-done
-echo --------- Recompiling v8 files in the translation directory -----------
-make clean
-make || { echo ---- Failed to recompile; exit 1; }
-echo --------- Saving v7 files in directory v7 -----------------------------
-/bin/rm -r ../v7
-mv /tmp/v7.$$ ../v7
-echo Saving v7 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 v8/$i $i
-done
-echo --------- Translation completed ---------------------------------------
-echo Old files are in directory '"v7"'
-echo New files are in current directory
-echo You can now remove the translation directory '"v8"'
diff --git a/tools/translate_V6-3-1_to_V7-0 b/tools/translate_V6-3-1_to_V7-0
deleted file mode 100755
index 10e7f140..00000000
--- a/tools/translate_V6-3-1_to_V7-0
+++ /dev/null
@@ -1,27 +0,0 @@
-#! /bin/sh
-
-echo "This shell script performs the following transformations:"
-echo "- Insertion of a space after a dot not followed by a separator"
-echo "- Insertion of a space between consecutive ~ and < and between"
-echo "  consecutive | and < assumed to be part of distinct tokens"
-echo "- Various renamings of commands as described in document Changes.ps"
-
-for i in $*
-  do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath/Add LoadPath/g" \
-    -e "s/~</~ </g" -e "s/|</| </g" \
-    -e "s/AddPath/Add LoadPath/g" -e "s/DelPath/Remove LoadPath/g" \
-    -e "s/AddRecPath/Add Rec LoadPath/g" \
-    -e "s/Implicit  *Arguments  *On/Set Implicit Arguments/g" \
-    -e "s/Implicit *Arguments *Off/Unset Implicit Arguments/g" \
-    -e "s/Begin *Silent/Set Silent/g" -e "s/End *Silent/Unset Silent/g" \
-    -e "s/Print *Path/Print Coercion Paths/g" \
-    $i > $i.tmp$$
-  if diff $i.tmp$$ $i > /dev/null
-    then
-      rm $i.tmp$$
-    else
-      echo Le fichier $i a été modifié
-      mv $i.tmp$$ $i
-  fi
-  done
-echo
diff --git a/tools/upgrade-v8 b/tools/upgrade-v8
deleted file mode 100755
index 36d0bf8c..00000000
--- a/tools/upgrade-v8
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/sh
-
-mv v7 v7.bak
-
-echo ---------------- Saving v7 files into directory v7 ------------------
-vfiles=`find . -name \*.v`
-for i in $vfiles; do
-  if expr $i : 'v7\.bak/.*\.v' > /dev/null ; then continue ; fi
-  if expr $i : 'v7/.*\.v' > /dev/null ; then continue ; fi
-  echo Saving $i into v7/$i
-  j=v7/$i
-  mkdir -p `dirname $j`
-  mv -u -f $i $j
-done
-
-echo ---------------- Upgrading files with v8 syntax ---------------------
-v8files=`find . -name \*.v8`
-for i in $v8files; do
-  j=`dirname $i`/`basename $i .v8`.v
-  echo Upgrading $i
-  mv -u -f $i $j
-done