Imported Upstream version 8.0pl1upstream/8.0pl1

28 files changed, 5171 insertions, 0 deletions

diff --git a/tools/README.coq-tex b/tools/README.coq-tex
new file mode 100755
index 00000000..5c7606a9
--- /dev/null
+++ b/tools/README.coq-tex
@@ -0,0 +1,13 @@
+DESCRIPTION.
+
+The coq-tex filter extracts Coq phrases embedded in LaTeX files,
+evaluates them, and insert the outcome of the evaluation after each
+phrase.
+
+The filter is written in Perl, so you'll need Perl version 4 installed
+on your machine.
+
+USAGE. See the manual page (coq-tex.1).
+
+AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr)
+  from caml-tex of Xavier Leroy.
diff --git a/tools/README.emacs b/tools/README.emacs
new file mode 100755
index 00000000..0d27b607
--- /dev/null
+++ b/tools/README.emacs
@@ -0,0 +1,31 @@
+
+DESCRIPTION:
+
+An emacs mode to help editing Coq vernacular files.
+
+AUTHOR:
+
+Jean-Christophe Filliatre (jcfillia@lri.fr),
+	from the Caml mode of Xavier Leroy.
+
+CONTENTS:
+
+    coq.el         A major mode for editing Coq files in Gnu Emacs
+
+USAGE:
+
+Add the following lines to your .emacs file:
+
+(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
+(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+
+The Coq major mode is triggered by visiting a file with extension .v,
+or manually by M-x coq-mode. It gives you the correct syntax table for
+the Coq language, and also a rudimentary indentation facility:
+
+- pressing TAB at the beginning of a line indents the line like the line above
+
+- extra TABs increase the indentation level (by 2 spaces by default)
+
+- M-TAB decreases the indentation level.
+
diff --git a/tools/check-v8 b/tools/check-v8
new file mode 100755
index 00000000..9dfa0be3
--- /dev/null
+++ b/tools/check-v8
@@ -0,0 +1,24 @@
+#!/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-inferior.el b/tools/coq-inferior.el
new file mode 100644
index 00000000..d4f96a16
--- /dev/null
+++ b/tools/coq-inferior.el
@@ -0,0 +1,324 @@
+;;; inferior-coq.el --- Run an inferior Coq process.
+;;;
+;;; Copyright (C) Marco Maggesi <maggesi@math.unifi.it>
+;;; Time-stamp: "2002-02-28 12:15:04 maggesi"
+
+
+;; Emacs Lisp Archive Entry
+;; Filename: inferior-coq.el
+;; Version: 1.0
+;; Keywords: process coq
+;; Author: Marco Maggesi <maggesi@math.unifi.it>
+;; Maintainer: Marco Maggesi <maggesi@math.unifi.it>
+;; Description: Run an inferior Coq process.
+;; URL: http://www.math.unifi.it/~maggesi/
+;; Compatibility: Emacs20, Emacs21, XEmacs21
+
+;; This is free software; you can redistribute it and/or modify it under
+;; the terms of the GNU General Public License as published by the Free
+;; Software Foundation; either version 2, or (at your option) any later
+;; version.
+;;
+;; This is distributed in the hope that it will be useful, but WITHOUT
+;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+;; FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+;; for more details.
+;;
+;; You should have received a copy of the GNU General Public License
+;; along with GNU Emacs; see the file COPYING.  If not, write to the
+;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+;; MA 02111-1307, USA.
+
+;;; Commentary:
+
+;; Coq is a proof assistant (http://coq.inria.fr/).  This code run an
+;; inferior Coq process and defines functions to send bits of code
+;; from other buffers to the inferior process.  This is a
+;; customisation of comint-mode (see comint.el).  For a more complex
+;; and full featured Coq interface under Emacs look at Proof General
+;; (http://zermelo.dcs.ed.ac.uk/~proofgen/).
+;;
+;; Written by Marco Maggesi <maggesi@math.unifi.it> with code heavly
+;; borrowed from emacs cmuscheme.el
+;;
+;; Please send me bug reports, bug fixes, and extensions, so that I can
+;; merge them into the master source.
+
+;;; Installation:
+
+;; You need to have coq.el already installed (it comes with the
+;; standard Coq distribution) in order to use this code.  Put this
+;; file somewhere in you load-path and add the following lines in your
+;; "~/.emacs":
+;;
+;;   (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
+;;   (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+;;   (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t)
+;;   (autoload 'run-coq-other-window "inferior-coq"
+;;     "Run an inferior Coq process in a new window." t)
+;;   (autoload 'run-coq-other-frame "inferior-coq"
+;;     "Run an inferior Coq process in a new frame." t)
+
+;;; Usage:
+
+;; Call `M-x "run-coq'.
+;;
+;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'):
+;;   C-return ('M-x coq-send-line)     send the current line.
+;;   C-c C-r  (`M-x coq-send-region')  send the current region.
+;;   C-c C-a  (`M-x coq-send-abort')   send the command "Abort".
+;;   C-c C-t  (`M-x coq-send-restart') send the command "Restart".
+;;   C-c C-s  (`M-x coq-send-show')    send the command "Show".
+;;   C-c C-u  (`M-x coq-send-undo')    send the command "Undo".
+;;   C-c C-v  (`M-x coq-check-region') run command "Check" on region.
+;;   C-c .    (`M-x coq-come-here')    Restart and send until current point.
+
+;;; Change Log:
+
+;; From -0.0 to 1.0 brought into existence.
+
+
+(require 'coq)
+(require 'comint)
+
+(setq coq-program-name "coqtop")
+
+(defgroup inferior-coq nil
+  "Run a coq process in a buffer."
+  :group 'coq)
+
+(defcustom inferior-coq-mode-hook nil
+  "*Hook for customising inferior-coq mode."
+  :type 'hook
+  :group 'coq)
+
+(defvar inferior-coq-mode-map
+  (let ((m (make-sparse-keymap)))
+    (define-key m "\C-c\C-r" 'coq-send-region)
+    (define-key m "\C-c\C-a" 'coq-send-abort)
+    (define-key m "\C-c\C-t" 'coq-send-restart)
+    (define-key m "\C-c\C-s" 'coq-send-show)
+    (define-key m "\C-c\C-u" 'coq-send-undo)
+    (define-key m "\C-c\C-v" 'coq-check-region)
+    m))
+
+;; Install the process communication commands in the coq-mode keymap.
+(define-key coq-mode-map [(control return)] 'coq-send-line)
+(define-key coq-mode-map "\C-c\C-r" 'coq-send-region)
+(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort)
+(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart)
+(define-key coq-mode-map "\C-c\C-s" 'coq-send-show)
+(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo)
+(define-key coq-mode-map "\C-c\C-v" 'coq-check-region)
+(define-key coq-mode-map "\C-c." 'coq-come-here)
+
+(defvar coq-buffer)
+
+(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq"
+  "\
+Major mode for interacting with an inferior Coq process.
+
+The following commands are available:
+\\{inferior-coq-mode-map}
+
+A Coq process can be fired up with M-x run-coq.
+
+Customisation: Entry to this mode runs the hooks on comint-mode-hook
+and inferior-coq-mode-hook (in that order).
+
+You can send text to the inferior Coq process from other buffers
+containing Coq source.
+
+Functions and key bindings (Learn more keys with `C-c C-h'):
+  C-return ('M-x coq-send-line)     send the current line.
+  C-c C-r  (`M-x coq-send-region')  send the current region.
+  C-c C-a  (`M-x coq-send-abort')   send the command \"Abort\".
+  C-c C-t  (`M-x coq-send-restart') send the command \"Restart\".
+  C-c C-s  (`M-x coq-send-show')    send the command \"Show\".
+  C-c C-u  (`M-x coq-send-undo')    send the command \"Undo\".
+  C-c C-v  (`M-x coq-check-region') run command \"Check\" on region.
+  C-c .    (`M-x coq-come-here')    Restart and send until current point.
+"
+  ;; Customise in inferior-coq-mode-hook
+  (setq comint-prompt-regexp "^[^<]* < *")
+  (coq-mode-variables)
+  (setq mode-line-process '(":%s"))
+  (setq comint-input-filter (function coq-input-filter))
+  (setq comint-get-old-input (function coq-get-old-input)))
+
+(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'"
+  "*Input matching this regexp are not saved on the history list.
+Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters."
+  :type 'regexp
+  :group 'inferior-coq)
+
+(defun coq-input-filter (str)
+  "Don't save anything matching `inferior-coq-filter-regexp'."
+  (not (string-match inferior-coq-filter-regexp str)))
+
+(defun coq-get-old-input ()
+  "Snarf the sexp ending at point."
+  (save-excursion
+    (let ((end (point)))
+      (backward-sexp)
+      (buffer-substring (point) end))))
+
+(defun coq-args-to-list (string)
+  (let ((where (string-match "[ \t]" string)))
+    (cond ((null where) (list string))
+	  ((not (= where 0))
+	   (cons (substring string 0 where)
+		 (coq-args-to-list (substring string (+ 1 where)
+						 (length string)))))
+	  (t (let ((pos (string-match "[^ \t]" string)))
+	       (if (null pos)
+		   nil
+		 (coq-args-to-list (substring string pos
+						 (length string)))))))))
+
+;;;###autoload
+(defun run-coq (cmd)
+  "Run an inferior Coq process, input and output via buffer *coq*.
+If there is a process already running in `*coq*', switch to that buffer.
+With argument, allows you to edit the command line (default is value
+of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
+\(after the `comint-mode-hook' is run).
+\(Type \\[describe-mode] in the process buffer for a list of commands.)"
+
+  (interactive (list (if current-prefix-arg
+			 (read-string "Run Coq: " coq-program-name)
+			 coq-program-name)))
+  (if (not (comint-check-proc "*coq*"))
+      (let ((cmdlist (coq-args-to-list cmd)))
+	(set-buffer (apply 'make-comint "coq" (car cmdlist)
+			   nil (cdr cmdlist)))
+	(inferior-coq-mode)))
+  (setq coq-program-name cmd)
+  (setq coq-buffer "*coq*")
+  (switch-to-buffer "*coq*"))
+;;;###autoload (add-hook 'same-window-buffer-names "*coq*")
+
+;;;###autoload
+(defun run-coq-other-window (cmd)
+  "Run an inferior Coq process, input and output via buffer *coq*.
+If there is a process already running in `*coq*', switch to that buffer.
+With argument, allows you to edit the command line (default is value
+of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
+\(after the `comint-mode-hook' is run).
+\(Type \\[describe-mode] in the process buffer for a list of commands.)"
+
+  (interactive (list (if current-prefix-arg
+			 (read-string "Run Coq: " coq-program-name)
+			 coq-program-name)))
+  (if (not (comint-check-proc "*coq*"))
+      (let ((cmdlist (coq-args-to-list cmd)))
+	(set-buffer (apply 'make-comint "coq" (car cmdlist)
+			   nil (cdr cmdlist)))
+	(inferior-coq-mode)))
+  (setq coq-program-name cmd)
+  (setq coq-buffer "*coq*")
+  (pop-to-buffer "*coq*"))
+;;;###autoload (add-hook 'same-window-buffer-names "*coq*")
+
+(defun run-coq-other-frame (cmd)
+  "Run an inferior Coq process, input and output via buffer *coq*.
+If there is a process already running in `*coq*', switch to that buffer.
+With argument, allows you to edit the command line (default is value
+of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
+\(after the `comint-mode-hook' is run).
+\(Type \\[describe-mode] in the process buffer for a list of commands.)"
+
+  (interactive (list (if current-prefix-arg
+			 (read-string "Run Coq: " coq-program-name)
+			 coq-program-name)))
+  (if (not (comint-check-proc "*coq*"))
+      (let ((cmdlist (coq-args-to-list cmd)))
+	(set-buffer (apply 'make-comint "coq" (car cmdlist)
+			   nil (cdr cmdlist)))
+	(inferior-coq-mode)))
+  (setq coq-program-name cmd)
+  (setq coq-buffer "*coq*")
+  (switch-to-buffer-other-frame "*coq*"))
+
+(defun switch-to-coq (eob-p)
+  "Switch to the coq process buffer.
+With argument, position cursor at end of buffer."
+  (interactive "P")
+  (if (get-buffer coq-buffer)
+      (pop-to-buffer coq-buffer)
+      (error "No current process buffer.  See variable `coq-buffer'"))
+  (cond (eob-p
+	 (push-mark)
+	 (goto-char (point-max)))))
+
+(defun coq-send-region (start end)
+  "Send the current region to the inferior Coq process."
+  (interactive "r")
+  (comint-send-region (coq-proc) start end)
+  (comint-send-string (coq-proc) "\n"))
+
+(defun coq-send-line ()
+  "Send the current line to the Coq process."
+  (interactive)
+  (save-excursion
+    (end-of-line)
+    (let ((end (point)))
+      (beginning-of-line)
+      (coq-send-region (point) end)))
+  (next-line 1))
+
+(defun coq-send-abort ()
+  "Send the command \"Abort.\" to the inferior Coq process."
+  (interactive)
+  (comint-send-string (coq-proc) "Abort.\n"))
+
+(defun coq-send-restart ()
+  "Send the command \"Restart.\" to the inferior Coq process."
+  (interactive)
+  (comint-send-string (coq-proc) "Restart.\n"))
+
+(defun coq-send-undo ()
+  "Reset coq to the initial state and send the region between the
+   beginning of file and the point."
+  (interactive)
+  (comint-send-string (coq-proc) "Undo.\n"))
+
+(defun coq-check-region (start end)
+  "Run the commmand \"Check\" on the current region."
+  (interactive "r")
+  (comint-proc-query (coq-proc)
+		     (concat "Check "
+			     (buffer-substring start end)
+			     ".\n")))
+
+(defun coq-send-show ()
+  "Send the command \"Show.\" to the inferior Coq process."
+  (interactive)
+  (comint-send-string (coq-proc) "Show.\n"))
+
+(defun coq-come-here ()
+  "Reset coq to the initial state and send the region between the
+   beginning of file and the point."
+  (interactive)
+  (comint-send-string (coq-proc) "Reset Initial.\n")
+  (coq-send-region 1 (point)))
+
+(defvar coq-buffer nil "*The current coq process buffer.")
+
+(defun coq-proc ()
+  "Return the current coq process.  See variable `coq-buffer'."
+  (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode)
+				      (current-buffer)
+				      coq-buffer))))
+    (or proc
+	(error "No current process.  See variable `coq-buffer'"))))
+
+(defcustom inferior-coq-load-hook nil
+  "This hook is run when inferior-coq is loaded in.
+This is a good place to put keybindings."
+  :type 'hook
+  :group 'inferior-coq)
+	
+(run-hooks 'inferior-coq-load-hook)
+
+(provide 'inferior-coq)
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
new file mode 100755
index 00000000..9f6e5480
--- /dev/null
+++ b/tools/coq-sl.sty
@@ -0,0 +1,37 @@
+% COQ style option, for use with the coq-latex filter.
+
+\typeout{Document Style option `coq-sl' <7 Apr 92>.}
+
+\ifcase\@ptsize
+    \font\sltt = cmsltt10
+\or \font\sltt = cmsltt10 \@halfmag
+\or \font\sltt = cmsltt10 \@magscale1
+\fi
+
+{\catcode`\^^M=\active %
+ \gdef\@coqinputline#1^^M{\tt Coq < #1\par} %
+ \gdef\@coqoutputline#1^^M{\sltt#1\par} } %
+\def\@coqblankline{\medskip}
+\chardef\@coqbackslash="5C
+
+\def\coq{
+  \bgroup
+  \flushleft
+  \parindent 0pt
+  \parskip 0pt
+  \let\do\@makeother\dospecials
+  \catcode`\^^M=\active
+  \catcode`\\=0
+  \catcode`\ \active
+  \frenchspacing
+  \@vobeyspaces
+  \let\?\@coqinputline
+  \let\:\@coqoutputline
+  \let\;\@coqblankline
+  \let\\\@coqbackslash
+}
+
+\def\endcoq{
+  \endflushleft
+  \egroup\noindent
+}
diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4
new file mode 100644
index 00000000..6987d78b
--- /dev/null
+++ b/tools/coq-tex.ml4
@@ -0,0 +1,292 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: coq-tex.ml4,v 1.5.2.1 2004/07/16 19:31:45 herbelin Exp $ *)
+
+(* coq-tex
+ * JCF, 16/1/98
+ * adapted from caml-tex (perl script written by Xavier Leroy)
+ *
+ * Perl isn't as portable as it pretends to be, and is quite difficult 
+ * to read and maintain... Let us rewrite the stuff in Caml! *)
+
+let _ =
+  match Sys.os_type with
+    | "Unix" -> ()
+    | _ -> begin
+      	print_string "This program only runs under Unix !\n";
+      	flush stdout;
+      	exit 1
+      end
+
+let linelen = ref 72
+let output = ref ""
+let output_specified = ref false
+let image = ref ""
+let cut_at_blanks = ref false
+let verbose = ref false
+let slanted = ref false
+let hrule = ref false
+let small = ref false
+
+let coq_prompt = Str.regexp "Coq < "
+let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
+
+let remove_prompt s = Str.replace_first any_prompt "" s
+
+(* First pass: extract the Coq phrases to evaluate from [texfile]
+ * and put them into the file [inputv] *)
+
+let begin_coq = Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
+let end_coq   = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
+
+let extract texfile inputv =
+  let chan_in = open_in texfile in
+  let chan_out = open_out inputv in
+  let rec inside () =
+    let s = input_line chan_in in
+    if Str.string_match end_coq s 0 then
+      outside ()
+    else begin
+      output_string chan_out (s ^ "\n");
+      inside ()
+    end
+  and outside () =
+    let s = input_line chan_in in
+    if Str.string_match begin_coq s 0 then
+      inside ()
+    else
+      outside ()
+  in
+  try
+    output_string chan_out 
+      ("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
+    outside ()
+  with End_of_file -> 
+    begin close_in chan_in; close_out chan_out end
+
+(* Second pass: insert the answers of Coq from [coq_output] into the
+ * TeX file [texfile]. The result goes in file [result]. *)
+
+let begin_coq_example =
+  Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
+let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
+let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
+let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
+let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
+
+let has_match r s =
+  try let _ = Str.search_forward r s 0 in true with Not_found -> false
+
+let percent = Str.regexp "%"
+let bang    = Str.regexp "!"
+let expos   = Str.regexp "^"
+
+let tex_escaped s =
+  let rec trans = parser
+    | [< s1 = (parser 
+		 | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> 
+		     "\\" ^ (String.make 1 c)
+		 | [< ''\\' >] -> "\\char'134" 
+		 | [< ''^'  >] -> "\\char'136" 
+		 | [< ''~'  >] -> "\\char'176"
+		 | [< '' '  >] -> "~"
+		 | [< ''<'  >] -> "{<}"
+		 | [< ''>'  >] -> "{>}"
+		 | [< 'c >]    -> String.make 1 c);
+	 s2 = trans >] -> s1 ^ s2
+    | [< >] -> ""
+  in 
+  trans (Stream.of_string s)
+
+let encapsule sl c_out s =
+  if sl then
+    Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s)
+  else
+    Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s)
+      
+let print_block c_out bl =
+  List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl
+
+let insert texfile coq_output result =
+  let c_tex = open_in texfile in
+  let c_coq = open_in coq_output in
+  let c_out = open_out result in
+  (* next_block k : this function reads the next block of Coq output
+   * removing the k leading prompts.
+   * it returns the block as a list of string) *)
+  let last_read = ref "" in
+  let next_block k =
+    if !last_read = "" then last_read := input_line c_coq;
+    (* skip k prompts *)
+    for i = 1 to k do
+      last_read := remove_prompt !last_read;
+    done;
+    (* read and return the following lines until a prompt is found *)
+    let rec read_lines () =
+      let s = input_line c_coq in
+      if Str.string_match any_prompt s 0 then begin
+	last_read := s; []
+      end else
+	s :: (read_lines ())
+    in
+    let first = !last_read in first :: (read_lines ())
+  in
+  (* we are just after \end{coq_...} block *)
+  let rec just_after () = 
+    let s = input_line c_tex in
+    if Str.string_match begin_coq_example s 0 then begin
+      inside (Str.matched_group 1 s <> "example*")
+             (Str.matched_group 1 s <> "example#") 0 false
+    end
+    else begin
+      if !hrule then output_string c_out "\\hrulefill\\\\\n";
+      output_string c_out "\\end{flushleft}\n";
+      if !small then output_string c_out "\\end{small}\n";
+      if Str.string_match begin_coq_eval s 0 then
+	eval 0     
+      else begin
+	output_string c_out (s ^ "\n");
+	outside ()
+      end	  
+    end
+  (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
+  and outside () =
+    let s = input_line c_tex in
+    if Str.string_match begin_coq_example s 0 then begin
+      if !small then output_string c_out "\\begin{small}\n";
+      output_string c_out "\\begin{flushleft}\n";
+      if !hrule then output_string c_out "\\hrulefill\\\\\n";
+      inside (Str.matched_group 1 s <> "example*")
+             (Str.matched_group 1 s <> "example#") 0 true
+    end else if Str.string_match begin_coq_eval s 0 then
+      eval 0
+    else begin
+      output_string c_out (s ^ "\n");
+      outside ()
+    end
+  (* we are inside a \begin{coq_example?} ... \end{coq_example?} block
+   * show_answers tells what kind of block it is
+   * k is the number of lines read until now *)
+  and inside show_answers  show_questions k first_block = 
+    let s = input_line c_tex in
+    if Str.string_match end_coq_example s 0 then begin
+      just_after ()
+    end else begin
+      if !verbose then Printf.printf "Coq < %s\n" s;
+      if (not first_block) & k=0 then output_string c_out "\\medskip\n";
+      if show_questions then encapsule false c_out ("Coq < " ^ s);
+      if has_match dot_end_line s then begin
+	let bl = next_block (succ k) in
+	if !verbose then List.iter print_endline bl; 
+	if show_answers then print_block c_out bl;
+	inside show_answers  show_questions 0 false
+      end else
+	inside show_answers  show_questions (succ k) first_block
+    end
+  (* we are inside a \begin{coq_eval} ... \end{coq_eval} block
+   * k is the number of lines read until now *)
+  and eval k =
+    let s = input_line c_tex in
+    if Str.string_match end_coq_eval s 0 then
+      outside ()
+    else begin
+      if !verbose then Printf.printf "Coq < %s\n" s;
+      if has_match dot_end_line s then
+       	let bl = next_block (succ k) in
+	if !verbose then List.iter print_endline bl;
+	eval 0
+      else
+       	eval (succ k)
+    end
+  in
+  try
+    let _ = next_block 0 in (* to skip the Coq banner *)
+    let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *)
+    outside ()
+  with End_of_file -> begin
+    close_in c_tex;
+    close_in c_coq;
+    close_out c_out
+  end
+
+(* Process of one TeX file *)
+
+let rm f = try Sys.remove f with _ -> ()
+
+let one_file texfile =
+  let inputv = Filename.temp_file "coq_tex" ".v" in
+  let coq_output = Filename.temp_file "coq_tex" ".coq_output"in
+  let result =
+    if !output_specified then
+      !output
+    else if Filename.check_suffix texfile ".tex" then
+      (Filename.chop_suffix texfile ".tex") ^ ".v.tex"
+    else
+      texfile ^ ".v.tex" 
+  in
+  try
+    (* 1. extract Coq phrases *)
+    extract texfile inputv;
+    (* 2. run Coq on input *)
+    let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv
+			   coq_output) 
+    in
+    (* 3. insert Coq output into original file *)
+    insert texfile coq_output result;
+    (* 4. clean up *)
+    rm inputv; rm coq_output
+  with e -> begin
+    rm inputv; rm coq_output;
+    raise e
+  end
+
+(* Parsing of the command line, check of the Coq command and process
+ * of all the files in the command line, one by one *)
+
+let files = ref []
+      
+let parse_cl () =
+  Arg.parse
+      [ "-o", Arg.String (fun s -> output_specified := true; output := s),
+	"output-file    Specifiy the resulting LaTeX file";
+	"-n", Arg.Int (fun n -> linelen := n),
+	"line-width     Set the line width";
+	"-image", Arg.String (fun s -> image := s),
+	"coq-image  Use coq-image as Coq command";
+	"-w", Arg.Set cut_at_blanks,
+	"               Try to cut lines at blanks";
+	"-v", Arg.Set verbose,
+	"               Verbose mode (show Coq answers on stdout)";
+	"-sl", Arg.Set slanted,
+	"              Coq answers in slanted font (only with LaTeX2e)";
+	"-hrule", Arg.Set hrule,
+	"           Coq parts are written between 2 horizontal lines";
+	"-small", Arg.Set small,
+	"           Coq parts are written in small font"
+      ]
+      (fun s -> files := s :: !files)
+      "coq-tex [options] file ..."
+
+let main () =
+  parse_cl ();
+  if !image = "" then begin
+    Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
+    image := "coqtop"
+  end;
+  if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin
+    Printf.printf "Error: ";
+    let _ = Sys.command (!image ^ " -batch") in
+    exit 1
+  end else begin
+    Printf.printf "Your version of coqtop seems OK\n";
+    flush stdout
+  end;
+  List.iter one_file (List.rev !files)
+
+let _ = Printexc.catch main ()
diff --git a/tools/coq.el b/tools/coq.el
new file mode 100644
index 00000000..0eb04d8d
--- /dev/null
+++ b/tools/coq.el
@@ -0,0 +1,182 @@
+;; coq.el --- Coq mode editing commands for Emacs
+;;
+;; Jean-Christophe Filliatre, march 1995
+;; Honteusement pompé de caml.el, Xavier Leroy, july 1993.
+;;
+;; modified by Marco Maggesi <maggesi@math.unifi.it> for coq-inferior
+
+(defvar coq-mode-map nil
+  "Keymap used in Coq mode.")
+(if coq-mode-map
+    ()
+  (setq coq-mode-map (make-sparse-keymap))
+  (define-key coq-mode-map "\t"      'coq-indent-command)
+  (define-key coq-mode-map "\M-\t"   'coq-unindent-command)
+  (define-key coq-mode-map "\C-c\C-c"   'compile)
+)
+
+(defvar coq-mode-syntax-table nil
+  "Syntax table in use in Coq mode buffers.")
+(if coq-mode-syntax-table
+    ()
+  (setq coq-mode-syntax-table (make-syntax-table))
+  ; ( is first character of comment start
+  (modify-syntax-entry ?\( "()1" coq-mode-syntax-table)
+  ; * is second character of comment start,
+  ; and first character of comment end
+  (modify-syntax-entry ?*  ". 23" coq-mode-syntax-table)
+  ; ) is last character of comment end
+  (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table)
+  ; quote is a string-like delimiter (for character literals)
+  (modify-syntax-entry ?' "\"" coq-mode-syntax-table)
+  ; quote is part of words
+  (modify-syntax-entry ?' "w" coq-mode-syntax-table)
+)
+
+(defvar coq-mode-indentation 2
+  "*Indentation for each extra tab in Coq mode.")
+
+(defun coq-mode-variables ()
+  (set-syntax-table coq-mode-syntax-table)
+  (make-local-variable 'paragraph-start)
+  (setq paragraph-start (concat "^$\\|" page-delimiter))
+  (make-local-variable 'paragraph-separate)
+  (setq paragraph-separate paragraph-start)
+  (make-local-variable 'paragraph-ignore-fill-prefix)
+  (setq paragraph-ignore-fill-prefix t)
+  (make-local-variable 'require-final-newline)
+  (setq require-final-newline t)
+  (make-local-variable 'comment-start)
+  (setq comment-start "(* ")
+  (make-local-variable 'comment-end)
+  (setq comment-end " *)")
+  (make-local-variable 'comment-column)
+  (setq comment-column 40)
+  (make-local-variable 'comment-start-skip)
+  (setq comment-start-skip "(\\*+ *")
+  (make-local-variable 'parse-sexp-ignore-comments)
+  (setq parse-sexp-ignore-comments nil)
+  (make-local-variable 'indent-line-function)
+  (setq indent-line-function 'coq-indent-command))
+
+;;; The major mode
+
+(defun coq-mode ()
+  "Major mode for editing Coq code.
+Tab at the beginning of a line indents this line like the line above.
+Extra tabs increase the indentation level.
+\\{coq-mode-map}
+The variable coq-mode-indentation indicates how many spaces are
+inserted for each indentation level."
+  (interactive)
+  (kill-all-local-variables)
+  (setq major-mode 'coq-mode)
+  (setq mode-name "coq")
+  (use-local-map coq-mode-map)
+  (coq-mode-variables)
+  (run-hooks 'coq-mode-hook))
+
+;;; Indentation stuff
+
+(defun coq-in-indentation ()
+  "Tests whether all characters between beginning of line and point
+are blanks."
+  (save-excursion
+    (skip-chars-backward " \t")
+    (bolp)))
+
+(defun coq-indent-command ()
+  "Indent the current line in Coq mode.
+When the point is at the beginning of an empty line, indent this line like
+the line above.
+When the point is at the beginning of an indented line
+\(i.e. all characters between beginning of line and point are blanks\),
+increase the indentation by one level.
+The indentation size is given by the variable coq-mode-indentation.
+In all other cases, insert a tabulation (using insert-tab)."
+  (interactive)
+  (let* ((begline
+          (save-excursion
+            (beginning-of-line)
+            (point)))
+         (current-offset
+          (- (point) begline))
+         (previous-indentation
+          (save-excursion
+            (if (eq (forward-line -1) 0) (current-indentation) 0))))
+    (cond ((and (bolp)
+                (looking-at "[ \t]*$")
+                (> previous-indentation 0))
+           (indent-to previous-indentation))
+          ((coq-in-indentation)
+           (indent-to (+ current-offset coq-mode-indentation)))
+          (t
+           (insert-tab)))))
+
+(defun coq-unindent-command ()
+  "Decrease indentation by one level in Coq mode.
+Works only if the point is at the beginning of an indented line
+\(i.e. all characters between beginning of line and point are blanks\).
+Does nothing otherwise."
+  (interactive)
+  (let* ((begline
+          (save-excursion
+            (beginning-of-line)
+            (point)))
+         (current-offset
+          (- (point) begline)))
+    (if (and (>= current-offset coq-mode-indentation)
+             (coq-in-indentation))
+        (backward-delete-char-untabify coq-mode-indentation))))
+
+;;; Hilight
+
+(cond 
+ (window-system
+  (setq hilit-mode-enable-list  '(not text-mode)
+        hilit-inhibit-hooks     nil
+        hilit-inhibit-rebinding nil)
+  
+  (require 'hilit19)
+       (setq  hilit-quietly t)
+       (hilit-set-mode-patterns
+        'coq-mode
+        '(;;comments
+          ("(\\*" "\\*)" comment)
+          ;;strings
+          (hilit-string-find ?' string)
+	  ;;directives
+          ("^[ \t]*\\(AddPath\\|DelPath\\|Add[ \t]+ML[ \t]+Path\\|Declare[ \t]+ML[ \t]+Module\\|Require\\|Export\\|Module\\|Opaque\\|Transparent\\|Section\\|Chapter\\|End\\|Load\\|Print\\|Show\\)[ \t]+[^.]*" nil include)
+	  ("Implicit[ \t]+Arguments[ \t]+\\(On\\|Off\\)[^.]*" nil include)
+          ;;grammar definitions
+	  ("^[ \t]*Syntax[ \t]+\\(tactic\\|command\\)" nil define)
+	  ("^[ \t]*Syntax[ \t]+\\(tactic\\|command\\)[ \t]*level[ \t]+[0-9]+[ \t]*" nil define)
+	  ("^[ \t]*level[ \t]+[0-9]+[ \t]*:" nil define)
+	  ("^[ \t]*Grammar.*" ":=" define)
+          ("^[ \t]*Tactic[ \t]+Definition" ":=" define) 
+	  ("^[ \t]*Token[^.]*" nil define)
+	  ("^[ \t]*\\(Coercion\\|Class\\|Infix\\)[ \t]+[[A-Za-z0-9$_\\']+" nil define)
+          ;;declarations
+	  ("^[ \t]*Recursive[ \t]+Definition[ \t]+[A-Za-z0-9$_\\']+" nil defun)
+          ("^[ \t]*Syntactic[ \t]+Definition[ \t]+[A-Za-z0-9$_\\']+" nil defun)
+          ("^[ \t]*Tactic[ \t]+Definition[ \t]+[A-Za-z0-9$_\\']+" nil defun)
+	  ("^[ \t]*Inductive[ \t]+\\(Set\\|Prop\\|Type\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun)
+	  ("^[ \t]*Mutual[ \t]+\\(Inductive\\|CoInductive\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun)
+	  ("^[ \t]*\\(Inductive\\|CoInductive\\|CoFixpoint\\|Definition\\|Local\\|Fixpoint\\|with\\|Record\\|Correctness\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun)
+	  ("^[ \t]*\\(Derive\\|Dependant[ \t]+Derive\\)[ \t]+\\(Inversion\\|Inversion_clear\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun)
+	  ("^[ \t]*\\(Variable\\|Parameter\\|Hypothesis\\).*" ":" defun)
+	  ("^[ \t]*\\(Global[ \t]+Variable\\).*" ":" defun)
+	  ("^[ \t]*\\(Realizer[ \t]+Program\\|Realizer\\)" nil defun)
+	  ;;proofs
+	  ("^[ \t]*\\(Lemma\\|Theorem\\|Remark\\|Axiom\\).*" ":" defun)
+	  ("^[ \t]*Proof" nil decl)
+	  ("^[ \t]*\\(Save\\|Qed\\|Defined\\|Hint\\|Immediate\\)[^.]*" nil decl)
+          ;;keywords
+          ("[^_]\\<\\(Case\\|Cases\\|case\\|esac\\|of\\|end\\|in\\|Match\\|with\\|Fix\\|let\\|if\\|then\\|else\\)\\>[^_]" 1 keyword)
+          ("[^_]\\<\\(begin\\|assert\\|invariant\\|variant\\|for\\|while\\|do\\|done\\|state\\)\\>[^_]" 1 keyword)
+          ))
+))
+
+;;; coq.el ends here
+
+(provide 'coq)
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
new file mode 100644
index 00000000..4879e97d
--- /dev/null
+++ b/tools/coq_makefile.ml4
@@ -0,0 +1,454 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: coq_makefile.ml4,v 1.16.2.1 2004/07/16 19:31:45 herbelin Exp $ *)
+
+(* créer un Makefile pour un développement Coq automatiquement *)
+
+type target =
+  | ML of string (* ML file : foo.ml -> (ML "foo") *)
+  | V of string  (* V file : foo.v -> (V "foo") *)
+  | Special of string * string * string (* file, dependencies, command *)
+  | Subdir of string
+  | Def of string * string (* X=foo -> Def ("X","foo") *)
+  | Include of string
+  | RInclude of string * string (* -R physicalpath logicalpath *)
+
+let output_channel = ref stdout
+let makefile_name = ref "Makefile"
+let make_name = ref ""
+
+let some_file = ref false
+let some_vfile = ref false
+let some_mlfile = ref false
+
+let opt = ref "-opt"
+let impredicative_set = ref false
+
+let print x = output_string !output_channel x
+let printf x = Printf.fprintf !output_channel x
+
+let rec print_list sep = function
+  | [ x ] -> print x
+  | x :: l -> print x; print sep; print_list sep l
+  | [] -> ()
+
+let section s =
+  let l = String.length s in
+  let sep = String.make (l+5) '#'
+  and sep2 = String.make (l+5) ' ' in
+  String.set sep (l+4) '\n';
+  String.set sep2 0 '#';
+  String.set sep2 (l+3) '#';
+  String.set sep2 (l+4) '\n';
+  print sep;
+  print sep2;
+  print "# "; print s; print " #\n";
+  print sep2;
+  print sep;
+  print "\n"
+
+let usage () =
+  output_string stderr "Usage summary:
+
+coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
+  command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath]
+  ... [VARIABLE = value] ...  [-opt|-byte] [-f file] [-o file] [-h] [--help]
+
+[file.v]: Coq file to be compiled
+[file.ml]: ML file to be compiled
+[subdirectory] : subdirectory that should be \"made\"
+[-custom command dependencies file]: add target \"file\" with command
+  \"command\" and dependencies \"dependencies\"
+[-I dir]: look for dependencies in \"dir\"
+[-R physicalpath logicalpath]: look for dependencies resursively starting from
+ \"physicalpath\". The logical path associated to the physical path is
+ \"logicalpath\".
+[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
+[-byte]: compile with byte-code version of coq
+[-opt]: compile with native-code version of coq
+[-impredicative-set]: compile with option -impredicative-set of coq
+[-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 =
+  print "byte:\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";
+  if !some_file then print "include .depend\n\n";
+  print ".depend depend:\n";
+  if !some_file then begin
+    print "\trm -f .depend\n";
+    print "\t$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend\n";
+    print "\t$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend\n";
+  end;
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n")
+    sds;
+  print "\n";
+  print "install:\n";
+  print "\tmkdir -p `$(COQC) -where`/user-contrib\n";
+  if !some_vfile then print "\tcp -f *.vo `$(COQC) -where`/user-contrib\n";
+  if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n";
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n")
+    sds;
+  print "\n";
+  if !make_name <> "" then begin
+    printf "%s: %s\n" !makefile_name !make_name;
+    printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name;
+    printf "\t$(COQBIN)coq_makefile -f %s -o %s\n" !make_name !makefile_name;
+    print "\n";
+    List.iter
+      (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n")
+      sds;
+    print "\n";
+  end;
+  print "clean:\n";
+  print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~\n";
+  print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n";
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n")
+    sds;
+  print "\n";
+  print "archclean:\n";
+  print "\trm -f *.cmx *.o\n";
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
+    sds;
+  print "\n";
+  print "html:\n";
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) html)\n")
+    sds;
+  print "\n"
+
+let implicit () =
+  let ml_rules () =
+    print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+    print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+    print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+  and v_rule () =
+    print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
+    print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
+    print ".v.g:\n\t$(GALLINA) $<\n\n";
+    print ".v.tex:\n\t$(COQDOC) -latex $< -o $@\n\n";
+    print ".v.html:\n\t$(COQDOC) -html $< -o $@\n\n";
+    print ".v.g.tex:\n\t$(COQDOC) -latex -g $< -o $@\n\n";
+    print ".v.g.html:\n\t$(COQDOC) -html -g $< -o $@\n\n"
+  and ml_suffixes =
+    if !some_mlfile then 
+      [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ]
+    else 
+      []
+  and v_suffixes =
+    if !some_vfile then 
+      [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ] 
+    else 
+      []
+  in
+  let suffixes = ml_suffixes @ v_suffixes in
+  if suffixes <> [] then begin
+    print ".SUFFIXES: "; print_list " " suffixes;
+    print "\n\n"
+  end;
+  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
+  section "Variables definitions.";
+  print "CAMLP4LIB=`camlp4 -where`\n";
+(*  print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *)
+  print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
+  -I $(COQTOP)/library -I $(COQTOP)/parsing \\
+  -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
+  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\
+  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \\
+  -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\
+  -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \\
+  -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\
+  -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\
+  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\
+  -I $(CAMLP4LIB)\n";
+  print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n";
+  if !opt = "-byte" then 
+    print "override OPT=-byte\n"
+  else
+    print "OPT=\n";
+  if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
+  print "COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
+  print "COQC=$(COQBIN)coqc\n";
+  print "GALLINA=gallina\n";
+  print "COQDOC=coqdoc\n";
+  print "CAMLC=ocamlc -c\n";
+  print "CAMLOPTC=ocamlopt -c\n";
+  print "CAMLLINK=ocamlc\n";
+  print "CAMLOPTLINK=ocamlopt\n";
+  print "COQDEP=$(COQBIN)coqdep -c\n";
+  print "GRAMMARS=grammar.cma\n";
+  print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n";
+  print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
+  var_aux l;
+  print "\n"
+
+let include_dirs l =
+  let include_aux' includeR =
+   let rec include_aux = function
+     | [] -> []
+     | Include x :: r -> ("-I " ^ x) :: (include_aux r)
+     | RInclude (p,l) :: r when includeR ->
+        let l' = if l = "" then "\"\"" else l in
+        ("-R " ^ p ^ " " ^ l') :: (include_aux r)
+     | _ :: r -> include_aux r
+   in
+    include_aux
+  in
+  let i_ocaml = "-I ." :: (include_aux' false l) in
+  let i_coq   = "-I ." :: (include_aux' true  l) in
+  section "Libraries definition.";
+  print "OCAMLLIBS="; print_list "\\\n  " i_ocaml; print "\n";
+  print "COQLIBS=";   print_list "\\\n  " i_coq; print "\n\n"
+
+let special l =
+  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
+
+let subdirs l =
+  let rec subdirs_aux = function
+    | [] -> []
+    | Subdir x :: r -> x :: (subdirs_aux r)
+    | _ :: r -> subdirs_aux r
+  and 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.";
+  print ".PHONY: ";
+  print_list " "
+    ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install" 
+     :: "depend" :: "html" :: sds);
+  print "\n\n";
+  sds
+
+(* Extract gallina/html filenames (foo.v) from the list of all targets *)
+
+let rec other_files suff = function
+  | V n :: r -> 
+      let f = (Filename.chop_suffix n ".vo") ^ suff in
+      f :: (other_files suff r)
+  | _   :: r -> 
+      other_files suff r
+  | [] -> 
+      []
+
+let vfiles = other_files ".v"
+let gfiles = other_files ".g"
+let hfiles = other_files ".html"
+let tfiles = other_files ".tex"
+let vifiles = other_files ".vi"
+let gtfiles l = List.map (fun f -> f ^ ".tex") (gfiles l)
+let ghfiles l = List.map (fun f -> f ^ ".html") (gfiles l)
+let vofiles = other_files ".vo"
+
+let all_target l =
+  let rec fnames = function
+    | ML n :: r -> n :: (fnames r)
+    | Subdir n :: r -> n :: (fnames r)
+    | V n :: r -> n :: (fnames r)
+    | Special (n,_,_) :: r -> n :: (fnames r)
+    | Include _ :: r -> fnames r
+    | RInclude _ :: r -> fnames r
+    | Def _ :: r -> fnames r
+    | [] -> []
+  in
+  section "Definition of the \"all\" target.";
+  print "VFILES="; print_list "\\\n  " (vfiles l); print "\n";
+  print "VOFILES=$(VFILES:.v=.vo)\n";
+  print "VIFILES=$(VFILES:.v=.vi)\n";
+  print "GFILES=$(VFILES:.v=.g)\n";
+  print "HTMLFILES=$(VFILES:.v=.html)\n";
+  print "GHTMLFILES=$(VFILES:.v=.g.html)\n";
+  print "\n";
+  print "all: "; print_list "\\\n  " (fnames l);
+  print "\n\n";
+  if !some_vfile then begin
+    print "spec: $(VIFILES)\n\n";
+    print "gallina: $(GFILES)\n\n";
+    print "html: $(HTMLFILES)\n\n";
+    print "gallinahtml: $(GHTMLFILES)\n\n";
+    print "all.ps: $(VFILES)\n";
+    print "\t$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
+    print "all-gal.ps: $(VFILES)\n";
+    print "\t$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
+    print "\n\n"
+  end
+
+let parse f =
+  let rec string = parser 
+    | [< '' ' | '\n' | '\t' >] -> ""
+    | [< 'c; s >] -> (String.make 1 c)^(string s)
+    | [< >] -> ""
+  and string2 = parser 
+    | [< ''"' >] -> ""
+    | [< 'c; s >] -> (String.make 1 c)^(string2 s)
+  and skip_comment = parser 
+    | [< ''\n'; s >] -> s
+    | [< 'c; s >] -> skip_comment s
+    | [< >] -> [< >]
+  and args = parser 
+    | [< '' ' | '\n' | '\t'; s >] -> args s
+    | [< ''#'; s >] -> args (skip_comment s)
+    | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s
+    | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s)
+    | [< >] -> []
+  in
+  let c = open_in f in
+  let res = args (Stream.of_channel c) in
+  close_in c;
+  res
+
+let rec process_cmd_line = function
+  | [] -> 
+      some_file := !some_file or !some_mlfile or !some_vfile; []
+  | ("-h"|"--help") :: _ -> 
+      usage ()
+  | ("-no-opt"|"-byte") :: r -> 
+      opt := "-byte"; process_cmd_line r
+  | ("-full"|"-opt") :: r -> 
+      opt := "-opt"; process_cmd_line r
+  | "-impredicative-set" :: r ->
+      impredicative_set := true; process_cmd_line r
+  | "-custom" :: com :: dependencies :: file :: r ->
+      some_file := true;
+      Special (file,dependencies,com) :: (process_cmd_line r)
+  | "-I" :: d :: r ->
+      Include d :: (process_cmd_line r)
+  | "-R" :: p :: l :: r ->
+      RInclude (p,l) :: (process_cmd_line r)
+  | ("-I"|"-custom") :: _ -> 
+      usage ()
+  | "-f" :: file :: r -> 
+      make_name := file;
+      process_cmd_line ((parse file)@r)
+  | ["-f"] -> 
+      usage ()
+  | "-o" :: file :: r -> 
+      makefile_name := file;
+      output_channel := (open_out file);
+      (process_cmd_line r)
+  | v :: "=" :: def :: r -> 
+      Def (v,def) :: (process_cmd_line r)
+  | f :: r ->
+      if Filename.check_suffix f ".v" then begin
+        some_vfile := true; 
+	V (f^"o") :: (process_cmd_line r)
+      end else if Filename.check_suffix f ".ml" then begin
+        some_mlfile := true; 
+	ML ((Filename.chop_suffix f "ml")^"cmo") :: (process_cmd_line r)
+      end else
+        Subdir f :: (process_cmd_line r)
+
+let banner () =
+  print
+"##############################################################################
+##                 The Calculus of Inductive Constructions                  ##
+##                                                                          ##
+##                                Projet Coq                                ##
+##                                                                          ##
+##                     INRIA                        ENS-CNRS                ##
+##              Rocquencourt                        Lyon                    ##
+##                                                                          ##
+##                                  Coq V7                                  ##
+##                                                                          ##
+##                                                                          ##
+##############################################################################
+
+"
+
+let warning () =
+  print "# WARNING\n#\n";
+  print "# This Makefile has been automagically generated by coq_makefile\n";
+  print "# Edit at your own risks !\n";
+  print "#\n# END OF WARNING\n\n"
+
+let print_list l = List.iter (fun x -> print x; print " ") l
+
+let command_line args =
+  print "#\n# This Makefile was generated by the command line :\n";
+  print "# coq_makefile ";
+  print_list args;
+  print "\n#\n\n"
+
+let directories_deps l =
+  let print_dep f dep = 
+    if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end
+  in
+  let rec iter ((dirs,before) as acc) = function
+    | [] -> 
+	()
+    | (Subdir d) :: l -> 
+	print_dep d before; iter (d :: dirs, d :: before) l
+    | (ML f) :: l ->
+	print_dep f dirs; iter (dirs, f :: before) l
+    | (V f) :: l ->
+	print_dep f dirs; iter (dirs, f :: before) l
+    | (Special (f,_,_)) :: l ->
+	print_dep f dirs; iter (dirs, f :: before) l
+    | _ :: l -> 
+	iter acc l
+  in
+  iter ([],[]) l
+
+let do_makefile args =
+  let l = process_cmd_line args in
+  banner ();
+  warning ();
+  command_line args;
+  variables l;
+  include_dirs l;
+  all_target l;
+  special l;
+  let sds = subdirs l in
+  implicit ();
+  standard sds;
+  (* TEST directories_deps l; *)
+  warning ();
+  if not (!output_channel == stdout) then close_out !output_channel;
+  exit 0
+
+let main () =
+  let args =
+    if Array.length Sys.argv = 1 then usage ();
+    List.tl (Array.to_list Sys.argv)
+  in
+  do_makefile args
+
+let _ = Printexc.catch main ()
+
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
new file mode 100755
index 00000000..ab7cef92
--- /dev/null
+++ b/tools/coqdep.ml
@@ -0,0 +1,537 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: coqdep.ml,v 1.15.2.1 2004/07/16 19:31:46 herbelin Exp $ *)
+
+open Printf
+open Coqdep_lexer
+open Unix
+
+let (/) = Filename.concat
+
+let file_concat l =
+  if l=[] then "<empty>" else
+    List.fold_left (/) (List.hd l) (List.tl l)
+
+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
+let option_i = ref false
+let option_sort = ref false
+
+let suffixe = ref ".vo"
+let suffixe_spec = ref ".vi"
+
+type dir = string option
+
+(* Files specified on the command line *)
+let mlAccu  = ref ([] : (string * string * dir) list) 
+and mliAccu = ref ([] : (string * string * dir) list) 
+and vAccu   = ref ([] : string list)
+
+(* Queue operations *)
+let addQueue q v = q := v :: !q
+
+let safe_addQueue clq q (k,v) =
+  try
+    let v2 = List.assoc k !q in
+    if v<>v2 then 
+      let rec add_clash = function
+          (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
+        | cl::cltl -> cl::add_clash cltl
+        | [] -> [(k,[v;v2])] in
+      clq := add_clash !clq
+  with Not_found -> addQueue q (k,v)
+
+(* Files found in the loadpaths *)
+let mlKnown     = ref ([] : (string * dir) list) 
+and mliKnown    = ref ([] : (string * dir) list) 
+and vKnown      = ref ([] : (string list * string) list) 
+and coqlibKnown = ref ([] : (string list * string) list)
+
+let clash_v = ref ([]: (string list * string list) list)
+
+
+let warning_module_notfound f s =
+  eprintf "*** Warning : in file %s, module " f;
+  eprintf "%s.v is required and has not been found in loadpath !\n"
+    (String.concat "." s);
+  flush stderr
+
+let warning_notfound f s =
+  eprintf "*** Warning : in file %s, the file " f;
+  eprintf "%s.v is required and has not been found !\n" s;
+  flush stderr
+
+let warning_clash file dir =
+  match List.assoc dir !clash_v with
+    (f1::f2::fl) ->
+      let f = Filename.basename f1 in
+      let d1 = Filename.dirname f1 in
+      let d2 = Filename.dirname f2 in
+      let dl = List.map Filename.dirname (List.rev fl) in
+      eprintf
+        "*** Warning : in file %s, \n    required module %s is ambiguous!\n    (found %s.v in "
+        file (String.concat "." dir) f;
+      List.iter (fun s -> eprintf "%s, " s) dl;
+      eprintf "%s and %s)\n" d2 d1
+  | _ -> assert false
+
+let safe_assoc verbose file k =
+  if verbose && List.mem_assoc k !clash_v then warning_clash file k;
+  List.assoc k !vKnown
+
+
+     
+let file_name = function
+  | (s,None)     -> file_concat s 
+  | (s,Some ".") -> file_concat s
+  | (s,Some d)   -> d / file_concat s
+
+let traite_fichier_ML md ext =
+  try 
+    let chan = open_in (md ^ ext) in 
+    let buf = Lexing.from_channel chan in 
+    let deja_vu = ref [md] in
+    let a_faire = ref "" in
+    let a_faire_opt = ref "" in
+    begin try 
+      while true do
+	let (Use_module str) = caml_action buf in
+	if List.mem str !deja_vu then 
+	  ()
+	else begin
+	  addQueue deja_vu str;
+          begin try
+            let mlidir = List.assoc str !mliKnown in
+            let filename = file_name ([str],mlidir) in
+      	    a_faire := !a_faire ^ " " ^ filename ^ ".cmi"; 
+          with Not_found ->
+            try
+              let mldir = List.assoc str !mlKnown in
+              let filename = file_name ([str],mldir) in
+              a_faire := !a_faire ^ " " ^ filename ^ ".cmo";
+            with Not_found -> ()
+          end;
+          begin try
+            let mldir = List.assoc str !mlKnown in
+            let filename = file_name ([str],mldir) in
+    	    a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmx"
+          with Not_found ->
+            try
+              let mlidir = List.assoc str !mliKnown in
+              let filename = file_name ([str],mlidir) in
+              a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmi"
+            with Not_found -> ()
+          end
+	end
+      done
+    with Fin_fichier -> ()
+    end;
+    close_in chan;
+    (!a_faire, !a_faire_opt)
+  with Sys_error _ -> ("","")
+
+let cut_prefix p s =
+  let lp = String.length p in
+  let ls = String.length s in
+  if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
+
+let canonize f = match Sys.os_type with
+  | "Win32" -> cut_prefix ".\\" f
+  | _ -> cut_prefix "./" f
+
+let sort () = 
+  let seen = Hashtbl.create 97 in
+  let rec loop file =
+    let file = canonize file in
+    if not (Hashtbl.mem seen file) then begin
+      Hashtbl.add seen file ();
+      let cin = open_in (file ^ ".v") in
+      let lb = Lexing.from_channel cin in
+      try
+	while true do
+	  match coq_action lb with
+	    | Require (_, s) ->
+		(try loop (List.assoc s !vKnown) with Not_found -> ())
+	    | RequireString (_, s) -> loop s
+	    | _ -> ()
+	done
+      with Fin_fichier ->
+	close_in cin;
+	printf "%s%s " file !suffixe
+    end
+  in
+  List.iter loop !vAccu
+
+let traite_fichier_Coq verbose f = 
+  try 
+    let chan = open_in f in 
+    let buf = Lexing.from_channel chan in 
+    let deja_vu_v = ref ([]: string list list)
+    and deja_vu_ml = ref ([] : string list) in
+    try 
+      while true do
+      	let tok = coq_action buf in
+	match tok with
+	  | Require (spec,str) ->
+	      if not (List.mem str !deja_vu_v) then begin
+	        addQueue deja_vu_v str;
+                try
+                  let file_str = safe_assoc verbose f str in
+                  printf " %s%s" (canonize file_str)
+                    (if spec then !suffixe_spec else !suffixe)
+                with Not_found -> 
+		  if verbose && not (List.mem_assoc str !coqlibKnown) then
+                    warning_module_notfound f str
+       	      end
+	  | RequireString (spec,s) -> 
+	      let str = Filename.basename s in
+	      if not (List.mem [str] !deja_vu_v) then begin
+	        addQueue deja_vu_v [str];
+                try
+                  let file_str = List.assoc [str] !vKnown in
+                  printf " %s%s" (canonize file_str)
+                    (if spec then !suffixe_spec else !suffixe)
+                with Not_found -> 
+                  begin try  let _ = List.assoc [str] !coqlibKnown in ()
+                  with Not_found -> warning_notfound f s end
+       	      end
+	  | Declare sl -> 
+	      List.iter 
+		(fun str ->
+		   if not (List.mem str !deja_vu_ml) then begin
+		     addQueue deja_vu_ml str;
+               	     try
+              	       let mldir = List.assoc str !mlKnown in
+              	       printf " %s.cmo" (file_name ([str],mldir))
+              	     with Not_found -> () 
+		   end)
+		sl
+	  | Load str -> 
+	      let str = Filename.basename str in
+	      if not (List.mem [str] !deja_vu_v) then begin
+	        addQueue deja_vu_v [str];
+                try
+                  let file_str = List.assoc [str] !vKnown in
+                  printf " %s.v" (canonize file_str)
+                with Not_found -> ()
+       	      end
+      done
+    with Fin_fichier -> ();
+      close_in chan
+  with Sys_error _ -> () 
+
+
+let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151
+						     
+let mL_dep_list b f = 
+  try 
+    Hashtbl.find dep_tab f
+  with Not_found ->
+    let deja_vu = ref ([] : string list) in 
+    try 
+      let chan = open_in f in 
+      let buf = Lexing.from_channel chan in 
+      try 
+	while true do
+	  let (Use_module str) = caml_action buf in
+	  if str = b then begin
+	    eprintf "*** Warning : in file %s the" f;
+	    eprintf " notation %s. is useless !\n" b;
+	    flush stderr
+	  end else
+            if not (List.mem str !deja_vu) then addQueue deja_vu str
+      	done; []
+      with Fin_fichier -> begin
+	close_in chan; 
+	let rl = List.rev !deja_vu in
+      	Hashtbl.add dep_tab f rl;
+	rl
+      end
+    with Sys_error _ -> []
+
+let affiche_Declare f dcl = 
+  printf "\n*** In file %s: \n" f;
+  printf "Declare ML Module";
+  List.iter (fun str -> printf " \"%s\"" str) dcl;
+  printf ".\n";
+  flush stdout
+
+let warning_Declare f dcl =
+  eprintf "*** Warning : in file %s, the ML modules" f;
+  eprintf " declaration should be\n";
+  eprintf "*** Declare ML Module";
+  List.iter (fun str -> eprintf " \"%s\"" str) dcl;
+  eprintf ".\n";
+  flush stderr
+
+let traite_Declare f = 
+  let decl_list = ref ([] : string list) in
+  let rec treat = function
+    | s :: ll -> 
+	if (List.mem_assoc s !mlKnown) & not (List.mem s !decl_list) then begin
+       	  let mldir = List.assoc s !mlKnown in
+	  let fullname = file_name ([s],mldir) in
+	  let depl = mL_dep_list s (fullname ^ ".ml") in
+	  treat depl;
+	  decl_list := s :: !decl_list
+	end;
+	treat ll
+    | [] -> ()
+  in
+  try
+    let chan = open_in f in
+    let buf = Lexing.from_channel chan in
+    begin try 
+      while true do
+      	let tok = coq_action buf in
+      	(match tok with
+	   | Declare sl -> 
+	       decl_list := [];
+	       treat sl;
+	       decl_list := List.rev !decl_list;
+	       if !option_D then 
+		 affiche_Declare f !decl_list
+	       else if !decl_list <> sl then
+		 warning_Declare f !decl_list
+	   | _ -> ())
+      done
+    with Fin_fichier -> () end;
+    close_in chan
+  with Sys_error _ -> ()
+
+let file_mem (f,_,d) =
+  let rec loop = function
+    | (f1,_,d1) :: l -> (f1 = f && d1 = d) || (loop l)
+    | _ -> false
+  in 
+  loop
+
+let mL_dependencies () =
+  List.iter 
+    (fun ((name,ext,dirname) as pairname) ->
+       let fullname = file_name ([name],dirname) in
+       let (dep,dep_opt) = traite_fichier_ML fullname ext in
+       printf "%s.cmo: %s%s" fullname fullname ext;
+       if file_mem pairname !mliAccu then printf " %s.cmi" fullname;
+       printf "%s\n" dep;
+       printf "%s.cmx: %s%s" fullname fullname ext;
+       if file_mem pairname !mliAccu then printf " %s.cmi" fullname;
+       printf "%s\n" dep_opt;
+       flush stdout)
+    (List.rev !mlAccu);
+  List.iter
+    (fun ((name,ext,dirname) as pairname) ->
+       let fullname = file_name ([name],dirname) in
+       let (dep,_) = traite_fichier_ML fullname ext in
+       printf "%s.cmi: %s%s" fullname fullname ext;
+       printf "%s\n" dep;
+       flush stdout)
+    (List.rev !mliAccu)
+
+let coq_dependencies () =
+  List.iter
+    (fun name ->
+       printf "%s%s: %s.v" name !suffixe name;
+       traite_fichier_Coq true (name ^ ".v");
+       printf "\n";
+       if !option_i then begin
+	 printf "%s%s: %s.v" name !suffixe_spec name;
+	 traite_fichier_Coq false (name ^ ".v");
+	 printf "\n";
+       end;
+       flush stdout)
+    (List.rev !vAccu)
+
+let declare_dependencies () =
+  List.iter
+    (fun name ->
+       traite_Declare (name^".v");      
+       flush stdout)
+    (List.rev !vAccu)
+
+let rec warning_mult suf l = 
+  let tab = Hashtbl.create 151 in
+  List.iter 
+    (fun (f,d) -> 
+       begin try 
+	 let d' = Hashtbl.find tab f in
+	 if (Filename.dirname (file_name ([f],d)))
+      	   <> (Filename.dirname (file_name ([f],d'))) then begin
+	     eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf);
+	     flush stderr
+	   end
+       with Not_found -> () end;
+       Hashtbl.add tab f d) 
+    l
+
+(* Gives the list of all the directories under [dir], including [dir] *)
+let all_subdirs root_dir log_dir =
+  let l = ref [(root_dir,[log_dir])] in
+  let add f = l := f :: !l in
+  let rec traverse phys_dir dir =
+    let dirh = handle_unix_error opendir phys_dir in
+    try
+      while true do
+	let f = readdir dirh in
+	if f <> "." && f <> ".." then
+	  let file = dir@[f] in
+          let filename = phys_dir/f in
+	  if (stat filename).st_kind = S_DIR then begin
+	    add (filename,file);
+	    traverse filename file
+	  end
+      done
+    with End_of_file ->
+      closedir dirh
+  in
+  traverse root_dir [log_dir]; List.rev !l
+
+let usage () =
+  eprintf
+  "[ usage: coqdep [-w] [-I dir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
+  flush stderr;
+  exit 1
+
+let add_coqlib_known dir_name f =
+  let complete_name = dir_name/f in
+  let lib_name = Filename.basename dir_name in
+  match try (stat complete_name).st_kind with _ -> S_BLK with 
+    | S_REG -> 
+	if Filename.check_suffix f ".vo" then
+	  let basename = Filename.chop_suffix f ".vo" in
+	  addQueue coqlibKnown ([basename],complete_name);
+	  addQueue coqlibKnown (["Coq";lib_name;basename],complete_name)
+    | _ -> ()
+
+let add_coqlib_directory dir_name = 
+  match try (stat dir_name).st_kind with _ -> S_BLK with 
+    | S_DIR -> 
+	(let dir = opendir dir_name in
+      	 try
+	   while true do add_coqlib_known dir_name (readdir dir) done
+	 with End_of_file -> closedir dir)
+    | _ -> ()
+
+let coqdep () =
+  let lg_command = Array.length Sys.argv in
+  if lg_command < 2 then usage ();
+  let rec treat old_dirname old_name =
+    let name = Filename.basename old_name 
+    and new_dirname = Filename.dirname old_name in
+    let dirname = 
+      match (old_dirname,new_dirname) with 
+	| (d, ".") -> d
+	| (None,d) -> Some d
+	| (Some d1,d2) -> Some (d1/d2) 
+    in
+    let complete_name = file_name ([name],dirname) in
+    match try (stat complete_name).st_kind with _ -> S_BLK with 
+      | S_DIR ->
+	  (if name <> "." & name <> ".." then
+	     let dir=opendir complete_name in
+             let newdirname = 
+               match dirname with 
+                 | None -> name
+                 | Some d -> d/name 
+	     in
+	     try 
+	       while true do treat (Some newdirname) (readdir dir) done
+	     with End_of_file -> closedir dir)
+      | S_REG -> 
+	  if Filename.check_suffix name ".ml" then
+	    let basename = Filename.chop_suffix name ".ml" in
+	    addQueue mlAccu (basename,".ml",dirname)
+	  else if Filename.check_suffix name ".ml4" then
+	    let basename = Filename.chop_suffix name ".ml4" in
+	    addQueue mlAccu (basename,".ml4",dirname)
+	  else if Filename.check_suffix name ".mli" then
+	    let basename = Filename.chop_suffix name ".mli" in
+	    addQueue mliAccu (basename,".mli",dirname)
+	  else if Filename.check_suffix name ".v" then
+	    let basename = Filename.chop_suffix name ".v" in
+	    addQueue vAccu (file_name ([basename], dirname))
+      | _ -> ()
+  in 
+  let add_known phys_dir log_dir f =
+    let complete_name = phys_dir/f in
+    match try (stat complete_name).st_kind with _ -> S_BLK with 
+	| S_REG ->
+	    if Filename.check_suffix f ".ml" then
+	      let basename = Filename.chop_suffix f ".ml" in
+	      addQueue mlKnown (basename,Some phys_dir)
+	    else if Filename.check_suffix f ".ml4" then
+	      let basename = Filename.chop_suffix f ".ml4" in
+	      addQueue mlKnown (basename,Some phys_dir)
+	    else if Filename.check_suffix f ".mli" then
+	      let basename = Filename.chop_suffix f ".mli" in
+	      addQueue mliKnown (basename,Some phys_dir)
+	    else if Filename.check_suffix f ".v" then
+	      let basename = Filename.chop_suffix f ".v" in
+              let name = log_dir@[basename] in
+              let file = phys_dir/basename in
+              let paths = [name;[basename]] in
+	      List.iter
+                (fun n -> safe_addQueue clash_v vKnown (n,file)) paths
+        | _ -> () in
+  let add_directory (phys_dir, log_dir) = 
+      match try (stat phys_dir).st_kind with _ -> S_BLK with 
+	| S_DIR -> 
+	    (let dir = opendir phys_dir in
+      	     try
+	       while true do
+                 add_known phys_dir log_dir (readdir dir) done
+	     with End_of_file -> closedir dir)
+        | _ -> ()
+  in
+  let add_rec_directory dir_name log_name =
+    List.iter add_directory (all_subdirs dir_name log_name)
+  in
+  let rec parse = function
+      | "-c" :: ll -> option_c := true; parse ll
+      | "-D" :: ll -> option_D := true; parse ll
+      | "-w" :: ll -> option_w := true; parse ll
+      | "-i" :: ll -> option_i := true; parse ll
+      | "-sort" :: ll -> option_sort := true; parse ll
+      | "-I" :: r :: ll -> add_directory (r, []); parse ll
+      | "-I" :: [] -> usage ()
+      | "-R" :: r :: ln :: ll -> add_rec_directory r ln; parse ll
+      | "-R" :: ([] | [_]) -> usage ()
+      | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll
+      | "-coqlib" :: [] -> usage ()
+      | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
+      | "-suffix" :: [] -> usage ()
+      | f :: ll -> treat None f; parse ll
+      | [] -> ()
+  in
+  add_directory (".", []);
+  parse (List.tl (Array.to_list Sys.argv));
+  List.iter
+    (fun (s,_) -> add_coqlib_directory s)
+    (all_subdirs (!coqlib/"theories") "Coq");
+  List.iter 
+    (fun (s,_) -> add_coqlib_directory s)
+    (all_subdirs (!coqlib/"contrib") "Coq");
+  mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu);
+  mlKnown  := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu);
+  warning_mult ".mli" !mliKnown;
+  warning_mult ".ml" !mlKnown;
+(*  warning_mult ".v" (List.map (fun (s,d) -> (file_concat s, d))
+  !vKnown);*)
+  if !option_sort then begin sort (); exit 0 end;
+  if !option_c && not !option_D then mL_dependencies ();
+  if not !option_D then coq_dependencies ();
+  if !option_w || !option_D then declare_dependencies ()
+
+let _ = Printexc.catch coqdep ()
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
new file mode 100755
index 00000000..4f5f172f
--- /dev/null
+++ b/tools/coqdep_lexer.mll
@@ -0,0 +1,231 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: coqdep_lexer.mll,v 1.6.6.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+  
+{
+
+  open Filename 
+  open Lexing
+   
+  type mL_token = Use_module of string
+
+  type spec = bool
+		
+  type coq_token = 
+    | Require of spec * string list
+    | RequireString of spec * string
+    | Declare of string list
+    | Load of string
+
+  let comment_depth = ref 0
+ 
+  exception Fin_fichier
+    
+  let module_name = ref []
+  let ml_module_name = ref ""
+		      
+  let specif = ref false
+		 
+  let mllist = ref ([] : string list)
+
+  let field_name s = String.sub s 1 (String.length s - 1)
+}
+
+let space = [' ' '\t' '\n' '\r']
+let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
+let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
+let identchar = 
+  ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+
+let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+
+let dot = '.' ( space+ | eof)
+
+rule coq_action = parse
+  | "Require" space+
+      { specif := false; opened_file lexbuf }
+  | "Require" space+ "Export" space+
+      { specif := false; opened_file lexbuf}
+  | "Require" space+ "Syntax" space+
+      { specif := false; opened_file lexbuf}
+  | "Require" space+ "Import" space+
+      { specif := false; opened_file lexbuf}
+  | "Declare" space+ "ML" space+ "Module" space+
+      { mllist := []; modules lexbuf}
+  | "Load" space+
+      { load_file lexbuf }
+  | "\""
+      { string lexbuf; coq_action lexbuf}
+  | "(*" (* "*)" *)
+      { comment_depth := 1; comment lexbuf; coq_action lexbuf }  
+  | eof 
+      { raise Fin_fichier} 
+  | _   
+      { coq_action lexbuf }
+
+and caml_action = parse
+  | [' ' '\010' '\013' '\009' '\012'] +
+      { caml_action lexbuf }
+  | "open" [' ' '\010' '\013' '\009' '\012']*
+        { caml_opened_file lexbuf }
+  | lowercase identchar*
+      { caml_action lexbuf }
+  | uppercase identchar*
+      { ml_module_name := Lexing.lexeme lexbuf;
+        qual_id lexbuf }
+  | ['0'-'9']+
+    | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
+    | '0' ['o' 'O'] ['0'-'7']+
+    | '0' ['b' 'B'] ['0'-'1']+
+      { caml_action lexbuf }
+  | ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)?
+      { caml_action lexbuf }
+  | "\""
+      { string lexbuf; caml_action lexbuf }
+  | "'" [^ '\\' '\''] "'"
+      { caml_action lexbuf }
+  | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'"
+      { caml_action lexbuf }
+  | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
+      { caml_action lexbuf }
+  | "(*" (* "*)" *)
+      { comment_depth := 1; comment lexbuf; caml_action lexbuf }
+  | "#" | "&"  | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".."
+   | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|"
+   | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-"
+   | "-."    { caml_action lexbuf }
+
+  | ['!' '?' '~']
+    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
+            { caml_action lexbuf }
+  | ['=' '<' '>' '@' '^' '|' '&' '$']
+    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
+            { caml_action lexbuf }
+  | ['+' '-']
+    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
+            { caml_action lexbuf }
+  | "**"
+    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
+            { caml_action lexbuf }
+  | ['*' '/' '%']
+    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
+            { caml_action lexbuf }
+  | eof { raise Fin_fichier }
+  | _ { caml_action lexbuf }
+
+and comment = parse
+  | "(*" (* "*)" *)
+      { comment_depth := succ !comment_depth; comment lexbuf }
+  | "*)"
+      { comment_depth := pred !comment_depth;
+        if !comment_depth > 0 then comment lexbuf }
+  | "'" [^ '\\' '\''] "'"
+      { comment lexbuf }
+  | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'"
+      { comment lexbuf }
+  | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
+      { comment lexbuf }
+  | eof
+      { raise Fin_fichier } 
+  | _ { comment lexbuf }
+
+and string = parse
+  | '"' (* '"' *)
+      { () }
+  | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] *
+      { string lexbuf }
+  | '\\' ['\\' '"' 'n' 't' 'b' 'r'] (*'"'*)
+      { string lexbuf }
+  | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9']
+      { string lexbuf }
+  | eof
+      { raise Fin_fichier }
+  | _
+      { string lexbuf }
+
+and load_file = parse
+  | '"' [^ '"']* '"' (*'"'*)
+      { let s = lexeme lexbuf in
+	let f = String.sub s 1 (String.length s - 2) in
+	skip_to_dot lexbuf;
+	Load (if check_suffix f ".v" then chop_suffix f ".v" else f) }
+  | coq_ident
+      { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
+  | eof	
+      { raise Fin_fichier }
+  | _
+      { load_file lexbuf }
+
+and skip_to_dot = parse
+  | dot { () }
+  | eof { () }
+  | _   { skip_to_dot lexbuf }
+
+and opened_file = parse
+  | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file lexbuf }
+  | space+
+      	       	{ opened_file lexbuf }
+  | "Implementation"
+                { opened_file lexbuf }
+  | "Specification"
+                { specif := true; opened_file lexbuf }
+  | coq_ident
+       	       	{ module_name := [Lexing.lexeme lexbuf];
+                  opened_file_fields lexbuf }
+
+  | '"' [^'"']* '"'   { (*'"'*)
+                        let lex = Lexing.lexeme lexbuf in
+      	       	       	let str = String.sub lex 1 (String.length lex - 2) in
+                        let str =
+                          if Filename.check_suffix str ".v" then
+                            Filename.chop_suffix str ".v"
+                          else str in
+			RequireString (!specif, str) }
+  | eof		      { raise Fin_fichier }
+  | _		      { opened_file lexbuf }
+
+and opened_file_fields = parse
+  | "(*" (* "*)" *)
+                { comment_depth := 1; comment lexbuf;
+                  opened_file_fields lexbuf }
+  | space+
+      	       	{ opened_file_fields lexbuf }
+  | coq_field
+       	       	{ module_name :=
+                    field_name (Lexing.lexeme lexbuf) :: !module_name;
+                  opened_file_fields lexbuf }
+  | dot               { Require (!specif, List.rev !module_name) }
+  | eof		      { raise Fin_fichier }
+  | _		      { opened_file_fields lexbuf }
+
+
+and modules = parse
+  | space+              { modules lexbuf }
+  | "(*" (* "*)" *)	{ comment_depth := 1; comment lexbuf;
+      	       	       	  modules lexbuf }
+  | '"' [^'"']* '"'
+        { let lex = (Lexing.lexeme lexbuf) in 
+	  let str = String.sub lex 1 (String.length lex - 2) in
+	  mllist := str :: !mllist; modules lexbuf }
+  | _   { (Declare (List.rev !mllist)) }   
+
+and qual_id = parse
+  | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !ml_module_name) }
+  | eof { raise Fin_fichier }
+  | _ { caml_action lexbuf }
+
+and caml_opened_file = parse
+  | uppercase identchar*
+      { let lex = (Lexing.lexeme lexbuf) in 
+        let str = String.sub lex 0 (String.length lex) in
+        (Use_module (String.uncapitalize str)) }
+  | eof {raise Fin_fichier }
+  | _ { caml_action lexbuf }
+
+
+
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
new file mode 100644
index 00000000..2418b6e1
--- /dev/null
+++ b/tools/coqdoc/alpha.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: alpha.ml,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+let norm_char c = match Char.uppercase c with
+  | '\192'..'\198' -> 'A'
+  | '\199' -> 'C'
+  | '\200'..'\203' -> 'E'
+  | '\204'..'\207' -> 'I'
+  | '\209' -> 'N'
+  | '\210'..'\214' -> 'O'
+  | '\217'..'\220' -> 'U'
+  | '\221' -> 'Y'
+  | c -> c
+
+let norm_string s =
+  let u = String.copy s in
+  for i = 0 to String.length s - 1 do
+    u.[i] <- norm_char s.[i]
+  done;
+  u
+
+let compare_char c1 c2 = match norm_char c1, norm_char c2 with
+  | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
+  | 'A'..'Z', _ -> -1
+  | _, 'A'..'Z' -> 1
+  | c1, c2 -> compare c1 c2
+
+let compare_string s1 s2 = 
+  let n1 = String.length s1 in
+  let n2 = String.length s2 in
+  let rec cmp i = 
+    if i == n1 || i == n2 then
+      n1 - n2
+    else
+      let c = compare_char s1.[i] s2.[i] in
+      if c == 0 then cmp (succ i) else c
+  in
+  cmp 0
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
new file mode 100644
index 00000000..46409c9a
--- /dev/null
+++ b/tools/coqdoc/alpha.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: alpha.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+(* Alphabetic order. *)
+
+val compare_char : char -> char -> int
+val compare_string : string -> string -> int
+
+(* Alphabetic normalization. *)
+
+val norm_char : char -> char
+val norm_string : string -> string
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
new file mode 100644
index 00000000..7f7aa9aa
--- /dev/null
+++ b/tools/coqdoc/coqdoc.sty
@@ -0,0 +1,58 @@
+
+% This is coqdoc.sty, by Jean-Christophe Filliâtre
+% This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc)
+%
+% You can modify the following macros to customize the appearance
+% of the document.
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{coqdoc}[2002/02/11]
+
+% Headings
+
+\usepackage{fancyhdr}
+\newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
+\newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
+\pagestyle{fancyplain}
+
+%BEGIN LATEX
+\plainheadrulewidth 0.4pt
+\plainfootrulewidth 0pt
+\lhead[\coqdocleftpageheader]{\leftmark}
+\rhead[\leftmark]{\coqdocrightpageheader}
+\cfoot{}
+%END LATEX
+
+% Hevea puts to much space with \medskip and \bigskip
+%HEVEA\renewcommand{\medskip}{}
+%HEVEA\renewcommand{\bigskip}{}
+
+% own name
+\newcommand{\coqdoc}{\textsf{coqdoc}}
+
+% pretty underscores (the package fontenc causes ugly underscores)
+%BEGIN LATEX
+\def\_{\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em}
+%END LATEX
+
+% macro for typesetting keywords
+\newcommand{\coqdockw}[1]{\textsf{#1}}
+
+% macro for typesetting identifiers
+\newcommand{\coqdocid}[1]{\textit{#1}}
+
+% 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}}
+
+% macro for typesetting the title of a module implementation
+\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}}
+
+%HEVEA\newcommand{\lnot}{\coqwkw{not}}
+%HEVEA\newcommand{\lor}{\coqwkw{or}}
+%HEVEA\newcommand{\land}{\&}
+
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
new file mode 100644
index 00000000..60c21387
--- /dev/null
+++ b/tools/coqdoc/index.mli
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: index.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+type coq_module = string
+
+type loc = int
+
+type entry_type = 
+  | Library
+  | Module
+  | Definition
+  | Inductive
+  | Constructor
+  | Lemma
+  | Variable
+  | Axiom
+  | TacticDefinition
+
+type index_entry = 
+  | Def of string * entry_type
+  | Ref of coq_module * string
+  | Mod of coq_module * string
+
+val find : coq_module -> loc -> index_entry
+
+val add_module : coq_module -> unit
+
+type module_kind = Local | Coqlib | Unknown
+
+val find_module : coq_module -> module_kind
+
+(*s Scan identifiers introductions from a file *)
+
+val scan_file : string -> coq_module -> unit
+
+(*s Read globalizations from a file (produced by coqc -dump-glob) *)
+
+val read_glob : string -> unit
+
+(*s Indexes *)
+
+type 'a index = { 
+  idx_name : string;
+  idx_entries : (char * (string * 'a) list) list;
+  idx_size : int }
+
+val all_entries : unit -> 
+      (coq_module * entry_type) index *
+      (entry_type * coq_module index) list
+
+val map : (string -> 'a -> 'b) -> 'a index -> 'b index
+
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
new file mode 100644
index 00000000..799825ad
--- /dev/null
+++ b/tools/coqdoc/index.mll
@@ -0,0 +1,327 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: index.mll,v 1.2.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+{
+
+open Filename
+open Lexing 
+open Printf
+
+type coq_module = string
+
+type loc = int
+
+type entry_type = 
+  | Library
+  | Module
+  | Definition
+  | Inductive
+  | Constructor
+  | Lemma
+  | Variable
+  | Axiom
+  | TacticDefinition
+
+type index_entry = 
+  | Def of string * entry_type
+  | Ref of coq_module * string
+  | Mod of coq_module * string
+
+let table = Hashtbl.create 97
+
+let current_module = ref ""
+
+let add_def loc ty id = Hashtbl.add table (!current_module, loc) (Def (id, ty))
+
+let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id))
+
+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 current_type = ref Library
+
+(* Coq modules *)
+
+let split_sp s = 
+  try
+    let i = String.rindex s '.' in
+    String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
+  with Not_found -> 
+    "", s
+
+let modules = Hashtbl.create 97
+let local_modules = Hashtbl.create 97
+
+let add_module m =
+  let _,id = split_sp m in
+  Hashtbl.add modules id m;
+  Hashtbl.add local_modules m ()
+
+type module_kind = Local | Coqlib | Unknown
+
+let coq_module m =
+  String.length m >= 4 && String.sub m 0 4 = "Coq."
+
+let find_module m =
+  if Hashtbl.mem local_modules m then 
+    Local
+  else if coq_module m then
+    Coqlib
+  else
+    Unknown
+
+let ref_module loc s =
+  try
+    let n = String.length s in
+    let i = String.rindex s ' ' in 
+    let id = String.sub s (i+1) (n-i-1) in
+    add_mod !current_module (loc+i+1) (Hashtbl.find modules id) id
+  with Not_found -> 
+    ()
+
+(* Building indexes *)
+
+type 'a index = { 
+  idx_name : string;
+  idx_entries : (char * (string * 'a) list) list;
+  idx_size : int }
+		  
+let map f i = 
+  { i with idx_entries = 
+      List.map 
+	(fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l)) 
+	i.idx_entries }
+
+let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
+
+let sort_entries el =
+  let t = Hashtbl.create 97 in
+  List.iter 
+    (fun c -> Hashtbl.add t c [])
+    ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N'; 
+     'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];  
+  List.iter 
+    (fun ((s,_) as e) -> 
+       let c = Alpha.norm_char s.[0] in 
+       let l = try Hashtbl.find t c with Not_found -> [] in
+       Hashtbl.replace t c (e :: l)) 
+    el;
+  let res = ref [] in
+  Hashtbl.iter 
+    (fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
+  List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
+    
+let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
+
+let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
+
+let type_name = function
+  | Library -> "library"
+  | Module -> "module"
+  | Definition -> "definition"
+  | Inductive -> "inductive"
+  | Constructor -> "constructor"
+  | Lemma -> "lemma"
+  | Variable -> "variable"
+  | Axiom -> "axiom"
+  | TacticDefinition -> "tactic"
+
+let all_entries () =
+  let gl = ref [] in
+  let add_g s m t = gl := (s,(m,t)) :: !gl in
+  let bt = Hashtbl.create 11 in
+  let add_bt t s m =
+    let l = try Hashtbl.find bt t with Not_found -> [] in
+    Hashtbl.replace bt t ((s,m) :: l)
+  in
+  let classify (m,_) e = match e with 
+    | Def (s,t) -> add_g s m t; add_bt t s m
+    | Ref _ | Mod _ -> ()
+  in
+  Hashtbl.iter classify table;
+  Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
+  { idx_name = "global"; 
+    idx_entries = sort_entries !gl; 
+    idx_size = List.length !gl },
+  Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; 
+				   idx_entries = sort_entries e; 
+				   idx_size = List.length e }) :: l) bt []
+
+}
+
+(*s Shortcuts for regular expressions. *)
+
+let space = 
+  [' ' '\010' '\013' '\009' '\012']
+let firstchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+let identchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
+   '\'' '0'-'9']
+let ident = 
+  firstchar identchar*
+
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
+let end_hide = "(*" space* "end" space+ "hide" space* "*)"
+
+(*s Indexing entry point. *)
+
+rule traverse = parse
+  | "Definition" space
+      { current_type := Definition; index_ident lexbuf; traverse lexbuf }
+  | "Tactic" space+ "Definition" space
+      { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf }
+  | ("Axiom" | "Parameter") space 
+      { current_type := Axiom; index_ident lexbuf; traverse lexbuf }
+  | "Fixpoint" space
+      { current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
+	traverse lexbuf }
+  | ("Lemma" | "Theorem") space
+      { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
+  | "Inductive" space
+      { current_type := Inductive; 
+	index_ident lexbuf; inductive lexbuf; traverse lexbuf }
+  | "Record" space
+      { current_type := Inductive; index_ident lexbuf; traverse lexbuf }
+  | "Module" (space+ "Type")? space
+      { current_type := Module; index_ident lexbuf; traverse lexbuf }
+(*i***
+  | "Variable" 's'? space
+      { current_type := Variable; index_idents lexbuf; traverse lexbuf }
+***i*)
+  | "Require" (space+ "Export")? space+ ident
+      { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf }
+  | begin_hide 
+      { skip_hide lexbuf; traverse lexbuf }
+  | "(*" 
+      { comment lexbuf; traverse lexbuf }
+  | '"'
+      { string lexbuf; traverse lexbuf }
+  | eof          
+      { () }
+  | _            
+      { traverse lexbuf }
+
+(*s Index one identifier. *)
+
+and index_ident = parse
+  | space+ 
+      { index_ident lexbuf }
+  | ident  
+      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) }
+  | eof    
+      { () }
+  | _      
+      { () }
+
+(*s Index identifiers separated by blanks and/or commas. *)
+
+and index_idents = parse
+  | space+ | ','
+      { index_idents lexbuf }
+  | ident  
+      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf);
+	index_idents lexbuf }
+  | eof    
+      { () }
+  | _
+      { skip_until_point lexbuf }
+
+(*s Index identifiers in an inductive definition (types and constructors). *)
+
+and inductive = parse
+  | '|' | ":=" space* '|'? 
+      { current_type := Constructor; index_ident lexbuf; inductive lexbuf }
+  | "with" space
+      { current_type := Inductive; index_ident lexbuf; inductive lexbuf }
+  | '.'    
+      { () }
+  | eof    
+      { () }
+  | _      
+      { inductive lexbuf }
+
+(*s Index identifiers in a Fixpoint declaration. *)
+
+and fixpoint = parse
+  | "with" space
+      { index_ident lexbuf; fixpoint lexbuf }
+  | '.' 
+      { () }
+  | eof    
+      { () }
+  | _      
+      { fixpoint lexbuf }
+
+(*s Skip a possibly nested comment. *)
+
+and comment = parse
+  | "*)" { () }
+  | "(*" { comment lexbuf; comment lexbuf }
+  | '"'  { string lexbuf; comment lexbuf }
+  | eof  { eprintf " *** Unterminated comment while indexing" }
+  | _    { comment lexbuf }
+
+(*s Skip a constant string. *)
+
+and string = parse
+  | '"'  { () }
+  | eof  { eprintf " *** Unterminated string while indexing" }
+  | _    { string lexbuf }
+
+(*s Skip everything until the next dot. *)
+
+and skip_until_point = parse
+  | '.'  { () }
+  | eof  { () }
+  | _    { skip_until_point lexbuf }
+
+(*s Skip everything until [(* end hide *)] *)
+
+and skip_hide = parse
+  | eof | end_hide { () }
+  | _ { skip_hide lexbuf }
+
+{
+  
+  let read_glob f = 
+    let c = open_in f in
+    let cur_mod = ref "" in
+    try
+      while true do
+	let s = input_line c in
+	let n = String.length s in
+	if n > 0 then begin
+	  match s.[0] with
+	    | 'F' -> 
+		cur_mod := String.sub s 1 (n - 1)
+	    | 'R' ->
+		(try
+		   let i = String.index s ' ' in
+		   let loc = int_of_string (String.sub s 1 (i - 1)) in
+		   let sp = String.sub s (i + 1) (n - i - 1) in
+		   let m',id = split_sp sp in
+		   add_ref !cur_mod loc m' id
+		 with Not_found -> 
+		   ())
+	    | _ -> ()
+	end
+      done
+    with End_of_file -> 
+      close_in c
+
+  let scan_file f m = 
+    current_module := m;
+    let c = open_in f in
+    let lb = from_channel c in
+    traverse lb;
+    close_in c
+}
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
new file mode 100644
index 00000000..66d2a993
--- /dev/null
+++ b/tools/coqdoc/main.ml
@@ -0,0 +1,420 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: main.ml,v 1.4.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+(* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
+ *  - handling of absolute filenames (function coq_module)
+ *  - coq_module: chop ./// (arbitrary amount of slashes), not only "./"
+ *  - function chop_prefix not useful anymore. Deleted.
+ *  - correct typo in usage message: "-R" -> "--R"
+ *  - shorten the definition of make_path
+ * This notice is made to comply with section 2.a of the GPLv2.
+ * It may be removed or abbreviated as far as I am concerned.
+ *)
+
+open Filename
+open Printf
+open Output
+open Pretty
+
+(*s \textbf{Usage.} Printed on error output. *)
+
+let usage () =
+  prerr_endline "";
+  prerr_endline "Usage: coqdoc <options and files>";
+  prerr_endline "  --html              produce a HTML document (default)";
+  prerr_endline "  --latex             produce a LaTeX document";
+  prerr_endline "  --texmacs           produce a TeXmacs document";
+  prerr_endline "  --dvi               output the DVI";
+  prerr_endline "  --ps                output the PostScript";
+  prerr_endline "  -o <file>           write output in file <file>";
+  prerr_endline "  -d <dir>            output files into directory <dir>";
+  prerr_endline "  -g                  (gallina) skip proofs";
+  prerr_endline "  -s                  (short) no titles for files";
+  prerr_endline "  -l                  light mode (only defs and statements)";
+  prerr_endline "  -t <string>         give a title to the document";
+  prerr_endline "  --body-only         suppress LaTeX/HTML header and trailer";
+  prerr_endline "  --no-index          do not output the index";
+  prerr_endline "  --multi-index       index split in multiple files";
+  prerr_endline "  --toc               output a table of contents";
+  prerr_endline "  --vernac <file>     consider <file> as a .v file";
+  prerr_endline "  --tex <file>        consider <file> as a .tex file";
+  prerr_endline "  -p <string>         insert <string> in LaTeX preamble";
+  prerr_endline "  --files-from <file> read file names to process in <file>";
+  prerr_endline "  --quiet             quiet mode";
+  prerr_endline "  --glob-from <file>  read Coq globalizations from file <file>";
+  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 "  -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 "";
+  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
+    output, so that when the output of [coqdoc] is redirected this header
+    is not (unless both standard and error outputs are redirected, of 
+    course). *)
+
+let banner () =
+  eprintf "This is coqdoc version %s, compiled on %s\n"
+    Coq_config.version Coq_config.compile_date;
+  flush stderr
+    
+
+(*s \textbf{Separation of files.} Files given on the command line are
+    separated according to their type, which is determined by their
+    suffix.  Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
+    files have suffix \verb!.tex!. *)
+
+let check_if_file_exists f =
+  if not (Sys.file_exists f) then begin
+    eprintf "\ncoqdoc: %s: no such file\n" f;
+    exit 1
+  end
+
+let paths = ref []
+
+let add_path m l = paths := (m,l) :: !paths
+
+let exists_dir dir =
+  try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false
+
+let add_rec_path f l =
+  let rec traverse abs rel =
+    add_path abs rel;
+    let dirh = Unix.opendir abs in
+    try
+      while true do
+	let f = Unix.readdir dirh in
+	if f <> "" && f.[0] <> '.' && f <> "CVS" then
+	  let abs' = Filename.concat abs f in
+	  try 
+	    if exists_dir abs' then  traverse abs' (rel ^ "." ^ f)
+	  with Unix.Unix_error _ -> 
+	    ()
+      done
+    with End_of_file ->
+      Unix.closedir dirh
+  in
+  if exists_dir f then traverse f l
+
+(* turn A/B/C into A.B.C *)
+let make_path = Str.global_replace (Str.regexp "/") ".";;
+
+let coq_module file = 
+(* TODO
+ * LEM:
+ * We should also remove things like "/./" in the middle of the filename,
+ * rewrite "/foo/../bar" to "/bar", recognise different paths that lead
+ * to the same file / directory (via symlinks), etc. The best way to do
+ * all this would be to use the libc function realpath() on _both_ p and
+ * file / f before comparing them.
+ *
+ * The semantics of realpath() on file symlinks might not be what we
+ * want... (But it is what we want on directory symlinks.) So, we would
+ * have to cook up our own version of realpath()?
+ *
+ * Do all target platforms have realpath()?
+ *)
+  let f = chop_extension file in
+  (* remove leading ./ and any number of slashes after *)
+  let f = Str.replace_first (Str.regexp "^\\./+") "" f in
+  if (Str.string_before f 1) = "/" then
+    (* f is an absolute path. Prefixes must be matched with the beginning of f,
+     * not prepended
+     *)
+    let rec trypath = function
+     | [] -> make_path f
+     | (p, lg) :: r ->
+         (* make sure p ends with a single '/'
+          * This guarantees that we don't match a file whose name is
+          * of the form p ^ "foo". It means we may miss p itself,
+          * but this does not matter: coqdoc doesn't do anything
+          * of a directory anyway. *)
+         let p = (Str.replace_first (Str.regexp "/*$") "/" p) in
+         let p_quoted = (Str.quote p) in
+         if (Str.string_match (Str.regexp p_quoted) f 0) then
+           make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f))
+        else
+           trypath r
+    in trypath !paths
+  else (* f is a relative path *)
+    let rec trypath = function
+      | [] -> 
+	  make_path f
+      | (p,lg) :: r ->
+	  let p_file = Filename.concat p file in
+	  if Sys.file_exists p_file then
+	    make_path (Filename.concat lg f)
+	  else
+	    trypath r
+    in trypath !paths;;
+
+let what_file f =
+  check_if_file_exists f;
+  if check_suffix f ".v" || check_suffix f ".g" then
+    Vernac_file (f, coq_module f)
+  else if check_suffix f ".tex" then
+    Latex_file f
+  else begin
+    eprintf "\ncoqdoc: don't know what to do with %s\n" f;
+    exit 1
+  end
+
+(*s \textbf{Reading file names from a file.} 
+    File names may be given
+    in a file instead of being given on the command
+    line. [(files_from_file f)] returns the list of file names contained
+    in the file named [f]. These file names must be separated by spaces,
+    tabulations or newlines.
+ *)
+
+let files_from_file f =
+  let files_from_channel ch =
+    let buf = Buffer.create 80 in
+    let l = ref [] in
+    try
+      while true do
+	match input_char ch with
+	  | ' ' | '\t' | '\n' ->
+	      if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
+	      Buffer.clear buf
+	  | c -> 
+	      Buffer.add_char buf c
+      done; []
+    with End_of_file ->
+      List.rev !l
+  in
+  try
+    check_if_file_exists f;
+    let ch = open_in f in
+    let l = files_from_channel ch in
+    close_in ch;l
+  with Sys_error s -> begin
+    eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
+    exit 1
+  end
+
+(*s \textbf{Parsing of the command line.} *)
+
+let output_file = ref ""
+let dvi = ref false
+let ps = ref false
+
+let parse () =
+  let files = ref [] in
+  let add_file f = files := f :: !files in
+  let rec parse_rec = function
+    | [] -> ()
+
+    | ("-nopreamble" | "--nopreamble" | "--no-preamble"
+    |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
+	header_trailer := false; parse_rec rem
+    | ("-p" | "--preamble") :: s :: rem ->
+	push_in_preamble s; parse_rec rem
+    | ("-p" | "--preamble") :: [] ->
+	usage ()
+    | ("-noindex" | "--noindex" | "--no-index") :: rem ->
+	index := false; parse_rec rem
+    | ("-multi-index" | "--multi-index") :: rem ->
+	multi_index := true; parse_rec rem
+    | ("-toc" | "--toc" | "--table-of-contents") :: rem ->
+	toc := true; parse_rec rem
+    | ("-o" | "--output") :: f :: rem ->
+	output_file := f; parse_rec rem
+    | ("-o" | "--output") :: [] -> 
+	usage ()
+    | ("-d" | "--directory") :: dir :: rem ->
+	output_dir := dir; parse_rec rem
+    | ("-d" | "--directory") :: [] -> 
+	usage ()
+    | ("-s" | "--short") :: rem ->
+	short := true; parse_rec rem
+    | ("-l" | "-light" | "--light") :: rem ->
+	gallina := true; light := true; parse_rec rem
+    | ("-g" | "-gallina" | "--gallina") :: rem ->
+	gallina := true; parse_rec rem
+    | ("-t" | "-title" | "--title") :: s :: rem ->
+	title := s; parse_rec rem
+    | ("-t" | "-title" | "--title") :: [] ->
+	usage ()
+    | ("-latex" | "--latex") :: rem ->
+	Output.target_language := LaTeX; parse_rec rem
+    | ("-dvi" | "--dvi") :: rem ->
+	Output.target_language := LaTeX; dvi := true; parse_rec rem
+    | ("-ps" | "--ps") :: rem ->
+	Output.target_language := LaTeX; ps := true; parse_rec rem
+    | ("-html" | "--html") :: rem ->
+	Output.target_language := HTML; parse_rec rem
+    | ("-texmacs" | "--texmacs") :: rem ->
+	Output.target_language := TeXmacs; parse_rec rem
+
+    | ("-charset" | "--charset") :: s :: rem ->
+	Output.charset := s; parse_rec rem
+    | ("-charset" | "--charset") :: [] ->
+	usage ()
+    | ("-inputenc" | "--inputenc") :: s :: rem ->
+	Output.inputenc := s; parse_rec rem
+    | ("-inputenc" | "--inputenc") :: [] ->
+	usage ()
+    | ("-raw-comments" | "--raw-comments") :: rem ->
+	Output.raw_comments := true; parse_rec rem
+    | ("-latin1" | "--latin1") :: rem ->
+	Output.set_latin1 (); parse_rec rem
+    | ("-utf8" | "--utf8") :: rem ->
+	Output.set_utf8 (); parse_rec rem
+
+    | ("-q" | "-quiet" | "--quiet") :: rem ->
+	quiet := true; parse_rec rem
+
+    | ("-h" | "-help" | "-?" | "--help") :: rem ->
+	banner (); usage ()
+    | ("-v" | "-version" | "--version") :: _ ->
+	banner (); exit 0
+
+    | ("-vernac-file" | "--vernac-file") :: f :: rem -> 
+	check_if_file_exists f;
+	add_file (Vernac_file (f, coq_module f)); parse_rec rem
+    | ("-vernac-file" | "--vernac-file") :: [] ->
+	usage ()
+    | ("-tex-file" | "--tex-file") :: f :: rem -> 
+	add_file (Latex_file f); parse_rec rem
+    | ("-tex-file" | "--tex-file") :: [] ->
+	usage ()
+    | ("-files" | "--files" | "--files-from") :: f :: rem ->
+	List.iter (fun f -> add_file (what_file f)) (files_from_file f); 
+	parse_rec rem
+    | ("-files" | "--files") :: [] ->
+	usage ()
+
+    | "-R" :: path :: log :: rem -> 
+	add_path path log; parse_rec rem
+    | "-R" :: ([] | [_]) ->
+	usage ()
+    | ("-glob-from" | "--glob-from") :: f :: rem ->
+	Index.read_glob f; parse_rec rem
+    | ("-glob-from" | "--glob-from") :: [] ->
+	usage ()
+    | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
+	Output.externals := false; parse_rec rem
+    | ("--coqlib" | "-coqlib") :: u :: rem ->
+	Output.coqlib := u; parse_rec rem
+    | ("--coqlib" | "-coqlib") :: [] ->
+	usage ()
+
+    | f :: rem -> 
+	add_file (what_file f); parse_rec rem
+  in 
+  parse_rec (List.tl (Array.to_list Sys.argv));
+  List.rev !files
+
+
+(*s The following function produces the output. The default output is
+    the \LaTeX\ document: in that case, we just call [Web.produce_document]. 
+    If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
+    we make calls to \verb!latex! or \verb!dvips!  accordingly. *)
+
+let locally dir f x =
+  let cwd = Sys.getcwd () in
+  try
+    Sys.chdir dir; let y = f x in Sys.chdir cwd; y
+  with e ->
+    Sys.chdir cwd; raise e
+
+let clean_temp_files basefile =
+  let remove f = try Sys.remove f with _ -> () in
+  remove (basefile ^ ".tex");
+  remove (basefile ^ ".log");
+  remove (basefile ^ ".aux");
+  remove (basefile ^ ".dvi");
+  remove (basefile ^ ".ps");
+  remove (basefile ^ ".haux");
+  remove (basefile ^ ".html")
+
+let clean_and_exit file res = clean_temp_files file; exit res
+
+let cat file =
+  let c = open_in file in
+  try
+    while true do print_char (input_char c) done
+  with End_of_file ->
+    close_in c
+
+let copy src dst =
+  let cin = open_in src 
+  and cout = open_out dst in
+  try
+    while true do Pervasives.output_char cout (input_char cin) done
+  with End_of_file ->
+    close_in cin; close_out cout
+
+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
+      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
+
+
+(*s \textbf{Main program.} Print the banner, parse the command line,
+    read the files and then call [produce_document] from module [Web]. *)
+
+let main () =
+  let files = parse () in
+  if not !quiet then banner ();
+  if List.length files > 0 then produce_output files
+
+let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
new file mode 100644
index 00000000..c10f3683
--- /dev/null
+++ b/tools/coqdoc/output.ml
@@ -0,0 +1,812 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: output.ml,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+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
+
+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 *)
+
+let build_table l = 
+  let h = Hashtbl.create 101 in
+  List.iter (fun key ->Hashtbl.add h  key ()) l;
+  function s -> try Hashtbl.find h s; true with Not_found -> false
+
+let is_keyword = 
+  build_table
+    [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
+      "CoInductive"; "Defined"; "Definition"; 
+      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
+      "Hypothesis"; "Hypotheses"; 
+      "Immediate"; "Implicit"; "Import"; "Inductive"; 
+      "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
+      "Module"; "Module Type"; "Declare Module";
+      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
+      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+      "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+      "Unset"; "Variable"; "Variables"; 
+      "Notation"; 
+      (*i (* correctness *)
+      "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if";
+      "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant";
+      "while"; i*)
+      (*i (* coq terms *)
+      "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*)
+       ]
+
+(*s Current Coq module *)
+
+let current_module = ref ""
+
+let set_module m = current_module := m; page_title := m
+
+(*s Common to both LaTeX and HTML *)
+
+let item_level = ref 0
+
+(*s Customized pretty-print *)
+
+let token_pp = Hashtbl.create 97
+
+let add_printing_token = Hashtbl.replace token_pp
+
+let find_printing_token tok = 
+  try Hashtbl.find token_pp tok with Not_found -> None, None
+
+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{\\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}";
+	  ]
+
+(*s Table of contents *)
+
+type toc_entry = 
+  | Toc_library of string
+  | Toc_section of int * (unit -> unit) * string
+
+let (toc_q : toc_entry Queue.t) = Queue.create ()
+
+let add_toc_entry e = Queue.add e toc_q
+
+let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r
+
+(*s LaTeX output *)
+
+module Latex = struct
+
+  (*s Latex preamble *)
+
+  let (preamble : string Queue.t) = Queue.create ()
+
+  let push_in_preamble s = Queue.add s preamble
+
+  let header () =
+    if !header_trailer then begin
+      printf "\\documentclass[12pt]{article}\n";
+      if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
+      printf "\\usepackage[T1]{fontenc}\n";
+      printf "\\usepackage{fullpage}\n";
+      printf "\\usepackage{coqdoc}\n";
+      Queue.iter (fun s -> printf "%s\n" s) preamble;
+      printf "\\begin{document}\n"
+    end;
+    output_string 
+      "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";
+    output_string
+      "%% This file has been automatically generated with the command\n";
+    output_string "%% ";
+    Array.iter (fun s -> printf "%s " s) Sys.argv;
+    printf "\n";
+    output_string
+      "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"
+
+  let trailer () =
+    if !header_trailer then begin
+      printf "\\end{document}\n"
+    end
+
+  let char c = match c with
+    | '\\' -> 
+	printf "\\symbol{92}"
+    | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> 
+	output_char '\\'; output_char c
+    | '^' | '~' -> 
+	output_char '\\'; output_char c; printf "{}"
+    | _ -> 
+	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 () = 
+    if not !short then begin
+      printf "\\coqdocmodule{"; 
+      raw_ident !current_module; 
+      printf "}\n\n"
+    end
+
+  let start_latex_math () = output_char '$'
+
+  let stop_latex_math () = output_char '$'
+
+  let start_verbatim () = printf "\\begin{verbatim}"
+
+  let stop_verbatim () = printf "\\end{verbatim}\n"
+
+  let indentation n = 
+    if n == 0 then 
+      printf "\\noindent\n"
+    else
+      let space = 0.5 *. (float n) in
+      printf "\\coqdocindent{%2.2fem}\n" space
+
+  let with_latex_printing f tok =
+    try 
+      (match Hashtbl.find token_pp tok with
+	 | Some s, _ -> output_string s
+	 | _ -> f tok)
+    with Not_found -> 
+      f tok
+
+  let ident s _ = 
+    if is_keyword s then begin
+      printf "\\coqdockw{"; raw_ident s; printf "}"
+    end else begin
+      printf "\\coqdocid{"; raw_ident s; printf "}"
+    end
+
+  let ident s l = with_latex_printing (fun s -> ident s l) s
+
+  let symbol = with_latex_printing raw_ident
+
+  let rec reach_item_level n = 
+    if !item_level < n then begin
+      printf "\n\\begin{itemize}\n\\item "; incr item_level;
+      reach_item_level n
+    end else if !item_level > n then begin
+      printf "\n\\end{itemize}\n"; decr item_level;
+      reach_item_level n
+    end
+
+  let item n =
+    let old_level = !item_level in
+    reach_item_level n;
+    if n <= old_level then printf "\n\\item "
+
+  let stop_item () = reach_item_level 0
+
+  let start_doc () = printf "\n\n\n\\noindent\n"
+
+  let end_doc () = stop_item (); printf "\n\n\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 -> "\\section{"
+    | 2 -> "\\subsection{"
+    | 3 -> "\\subsubsection{"
+    | 4 -> "\\paragraph{"
+    | _ -> assert false
+
+  let section lev f =
+    stop_item ();
+    output_string (section_kind lev);
+    f ();
+    printf "}\n\n"
+
+  let rule () =
+    printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}"
+
+  let paragraph () = stop_item (); printf "\n\n\\medskip\n"
+
+  let line_break () = printf "\\coqdoceol\n"
+
+  let empty_line_of_code () = printf "\n\n\\medskip\n"
+
+  let start_inline_coq () = ()
+
+  let end_inline_coq () = ()
+
+  let make_index () = ()
+
+  let make_toc () = printf "\\tableofcontents\n"
+
+end
+
+
+(*s HTML output *)
+
+module Html = struct
+
+  let header () =
+    if !header_trailer then begin
+      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 "<title>%s</title>\n</head>\n\n" !page_title;
+      printf "<body>\n\n"
+    end
+
+  let self = "http://www.lri.fr/~filliatr/coqdoc/"
+
+  let trailer () =
+    if !index && !current_module <> "Index" then 
+      printf "<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>"
+    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
+    end
+
+  let indentation n = for i = 1 to n do printf "&nbsp;" done
+
+  let line_break () = printf "<br/>\n"
+
+  let empty_line_of_code () = printf "\n<br/>\n"
+
+  let char = function
+    | '<' -> printf "&lt;"
+    | '>' -> printf "&gt;"
+    | '&' -> printf "&amp;"
+    | c -> output_char c
+
+  let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done
+
+  let latex_char _ = ()
+  let latex_string _ = ()
+
+  let html_char = output_char
+  let html_string = output_string
+
+  let start_latex_math () = ()
+  let stop_latex_math () = ()
+
+  let start_verbatim () = printf "<pre>"
+  let stop_verbatim () = printf "</pre>\n"
+
+  let module_ref m s = 
+    printf "<a 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 s = match find_module m with
+    | Local ->
+	printf "<a 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>"
+    | Coqlib | Unknown ->
+	raw_ident s
+
+  let ident s loc = 
+    if is_keyword s then begin
+      printf "<code class=\"keyword\">"; 
+      raw_ident s; 
+      printf "</code>"
+    end else 
+      try
+	(match Index.find !current_module loc with
+	   | Def _ -> 
+	       printf "<a name=\"%s\"></a>" s; raw_ident s
+           | Mod (m,s') when s = s' ->
+	       module_ref m s
+	   | Ref (m,s') when s = s' -> 
+	       ident_ref m s
+	   | Mod _ | Ref _ ->
+	       raw_ident s)
+      with Not_found ->
+	raw_ident s
+	  
+  let with_html_printing f tok =
+    try 
+      (match Hashtbl.find token_pp tok with
+	 | _, Some s -> output_string s
+	 | _ -> f tok)
+    with Not_found -> 
+      f tok
+
+  let ident s l = with_html_printing (fun s -> ident s l) s
+
+  let symbol = with_html_printing raw_ident
+
+  let rec reach_item_level n = 
+    if !item_level < n then begin
+      printf "\n<ul>\n<li>"; incr item_level;
+      reach_item_level n
+    end else if !item_level > n then begin
+      printf "\n</li>\n</ul>\n"; decr item_level;
+      reach_item_level n
+    end
+
+  let item n =
+    let old_level = !item_level in
+    reach_item_level n;
+    if n <= old_level then printf "\n</li>\n<li>"
+
+  let stop_item () = reach_item_level 0
+
+  let start_coq () = if not !raw_comments then printf "<code>\n"
+
+  let end_coq () = if not !raw_comments then printf "</code>\n"
+
+  let start_doc () = 
+    if not !raw_comments then
+      printf "\n<table width=\"100%%\"><tr class=\"doc\"><td>\n"
+
+  let end_doc () =
+    stop_item (); 
+    if not !raw_comments then printf "\n</td></tr></table>\n"
+
+  let start_code () = end_doc (); start_coq ()
+
+  let end_code () = end_coq (); start_doc ()
+
+  let start_inline_coq () = printf "<code>"
+
+  let end_inline_coq () = printf "</code>"
+
+  let paragraph () = stop_item (); printf "\n<br/><br/>\n"
+
+  let section lev f =
+    let lab = new_label () in
+    let r = sprintf "%s.html#%s" !current_module lab in
+    add_toc_entry (Toc_section (lev, f, r));
+    stop_item ();
+    printf "<a name=\"%s\"></a><h%d>" lab lev;
+    f ();
+    printf "</h%d>\n" lev
+
+  let rule () = printf "<hr/>\n"
+
+  let entry_type = function
+    | Library -> "library"
+    | Module -> "module"
+    | Definition -> "definition"
+    | Inductive -> "inductive"
+    | Constructor -> "constructor"
+    | Lemma -> "lemma"
+    | Variable -> "variable"
+    | Axiom -> "axiom"
+    | TacticDefinition -> "tactic definition"
+
+  (* make a HTML index from a list of triples (name,text,link) *)
+  let index_ref i c =
+    let idxc = sprintf "%s_%c" i.idx_name c in
+    if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc
+
+  let letter_index category idx (c,l) =
+    if l <> [] then begin
+      let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
+      printf "<a name=\"%s_%c\"></a><h2>%c %s</h2>\n" idx c c cat;
+      List.iter 
+	(fun (id,(text,link)) -> 
+	   printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l;
+      printf "<br/><br/>"
+    end
+		
+  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
+
+  let format_global_index =
+    Index.map 
+      (fun s (m,t) -> 
+	 if t = Library then 
+	   "[library]", m ^ ".html"
+	 else
+	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m ,
+	   sprintf "%s.html#%s" m s)
+
+  let format_bytype_index = function
+    | Library, idx ->
+	Index.map (fun id m -> "", m ^ ".html") idx
+    | (t,idx) ->
+	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
+
+  let navig_one_index i =
+    printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
+    List.iter 
+      (fun (c,l) -> 
+	 if l <> [] then
+	   printf "<td><a href=\"%s\">%c</a></td>\n" (index_ref i c) c
+	 else
+	   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"
+
+  let navig_index il = 
+    printf "<table>\n";
+    List.iter navig_one_index il;
+    printf "</table>\n"
+
+  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";
+      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
+
+  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 ();
+	  printf "<a href=\"%s.html\"><h2>Library %s</h2></a>\n" m m
+      | Toc_section (n, f, r) ->
+	  item n; 
+	  printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+    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
+
+
+(*s TeXmacs-aware output *)
+
+module TeXmacs = struct
+
+  (*s Latex preamble *)
+
+  let in_doc = ref false
+
+  let (preamble : string Queue.t) = 
+    in_doc := false; Queue.create ()
+
+  let push_in_preamble s = Queue.add s preamble
+
+  let header () =
+    output_string 
+      "(*i This file has been automatically generated with the command  \n";
+    output_string 
+      "    "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n"
+
+  let trailer () = ()
+
+  let char_true c = match c with
+    | '\\' -> printf "\\\\"
+    | '<' -> printf "\\<"
+    | '|' -> printf "\\|"
+    | '>' -> printf "\\>"
+    | _ -> output_char c
+
+  let char c = if !in_doc then char_true c else output_char c
+
+  let latex_char = char_true
+  let latex_string = String.iter latex_char
+
+  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 start_latex_math () = printf "<with|mode|math|"
+
+  let stop_latex_math () = output_char '>'
+
+  let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+
+  let stop_verbatim () = in_doc := false; printf "</verbatim>"
+
+  let indentation n = ()
+
+  let ident_true s = 
+    if is_keyword s then begin
+      printf "<kw|"; raw_ident s; printf ">"
+    end else begin
+      raw_ident s
+    end
+
+  let ident s _ = if !in_doc then ident_true s else raw_ident s
+ 
+  let symbol_true s = 
+    let ensuremath x = printf "<with|mode|math|\\<%s\\>>" x in
+      match s with
+	| "*"  -> ensuremath "times"
+	| "->" -> ensuremath "rightarrow"
+	| "<-" -> ensuremath "leftarrow"
+	| "<->" ->ensuremath "leftrightarrow"
+	| "=>" -> ensuremath "Rightarrow"
+	| "<=" -> ensuremath "le"
+	| ">=" -> ensuremath "ge"
+	| "<>" -> ensuremath "noteq"
+	| "~" ->  ensuremath "lnot"
+	| "/\\" -> ensuremath "land"
+	| "\\/" -> ensuremath "lor"
+	| "|-" -> ensuremath "vdash"
+	| s    -> raw_ident s
+
+  let symbol s = if !in_doc then symbol_true s else raw_ident s
+
+  let rec reach_item_level n = 
+    if !item_level < n then begin
+      printf "\n<\\itemize>\n<item>"; incr item_level;
+      reach_item_level n
+    end else if !item_level > n then begin
+      printf "\n</itemize>"; decr item_level;
+      reach_item_level n
+    end
+
+  let item n =
+    let old_level = !item_level in
+    reach_item_level n;
+    if n <= old_level then printf "\n\n<item>"
+
+  let stop_item () = reach_item_level 0
+
+  let start_doc () = in_doc := true; printf "(** texmacs: "
+
+  let end_doc () = stop_item (); in_doc := false; printf " *)"
+
+  let start_coq () = ()
+
+  let end_coq () = ()
+
+  let start_code () = in_doc := true; printf "<\\code>\n"
+  let end_code () = in_doc := false; printf "\n</code>"
+
+  let section_kind = function
+    | 1 -> "section"
+    | 2 -> "subsection"
+    | 3 -> "subsubsection"
+    | 4 -> "paragraph"
+    | _ -> assert false
+
+  let section lev f =
+    stop_item ();
+    printf "<"; output_string (section_kind lev); printf "|"; 
+    f (); printf ">\n\n"
+
+  let rule () =
+    printf "\n<hrule>\n"
+
+  let paragraph () = stop_item (); printf "\n\n"
+
+  let line_break_true () = printf "<format|line break>"
+
+  let line_break () = printf "\n"
+
+  let empty_line_of_code () = printf "\n"
+
+  let start_inline_coq () = printf "<verbatim|["
+
+  let end_inline_coq () = printf "]>"
+
+  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 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 start_module = 
+  select Latex.start_module Html.start_module TeXmacs.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_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_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_inline_coq = 
+  select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq
+let end_inline_coq = 
+  select Latex.end_inline_coq Html.end_inline_coq TeXmacs.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 empty_line_of_code = select 
+  Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.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 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 latex_char = select Latex.latex_char Html.latex_char TeXmacs.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
+let html_string = 
+  select Latex.html_string Html.html_string TeXmacs.html_string
+
+let start_latex_math = 
+  select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math
+let stop_latex_math = 
+  select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math
+
+let start_verbatim = 
+  select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim
+let stop_verbatim = 
+  select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim
+let verbatim_char = 
+  select output_char Html.char TeXmacs.char
+let hard_verbatim_char = output_char
+
+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
new file mode 100644
index 00000000..2195fa53
--- /dev/null
+++ b/tools/coqdoc/output.mli
@@ -0,0 +1,92 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: output.mli,v 1.3.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+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
+
+val set_module : coq_module -> unit
+
+val header : unit -> unit
+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
+val end_doc : unit -> unit
+
+val start_coq : unit -> unit
+val end_coq : unit -> unit
+
+val start_code : unit -> unit
+val end_code : unit -> unit
+
+val start_inline_coq : unit -> unit
+val end_inline_coq : unit -> unit
+
+val indentation : int -> unit
+val line_break : unit -> unit
+val paragraph : unit -> unit
+val empty_line_of_code : unit -> unit
+
+val section : int -> (unit -> unit) -> unit
+
+val item : int -> unit
+
+val rule : unit -> unit
+
+val char : char -> unit
+val ident : string -> loc -> unit
+val symbol : string -> unit
+
+val latex_char : char -> unit
+val latex_string : string -> unit
+val html_char : char -> unit
+val html_string : string -> unit
+val verbatim_char : char -> unit
+val hard_verbatim_char : char -> unit
+
+val start_latex_math : unit -> unit
+val stop_latex_math : unit -> unit
+val start_verbatim : unit -> unit
+val stop_verbatim : unit -> unit
+
+val make_index : unit -> unit
+val make_toc : unit -> unit
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli
new file mode 100644
index 00000000..07808fe9
--- /dev/null
+++ b/tools/coqdoc/pretty.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: pretty.mli,v 1.1.2.1 2004/07/16 19:31:47 herbelin Exp $ 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
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
new file mode 100644
index 00000000..541939b5
--- /dev/null
+++ b/tools/coqdoc/pretty.mll
@@ -0,0 +1,586 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: pretty.mll,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+(*s Utility functions for the scanners *)
+
+{
+
+  open Printf
+  open Index
+  open Lexing 
+  open Output
+
+  (* count the number of spaces at the beginning of a string *)
+  let count_spaces s =
+    let n = String.length s in
+    let rec count c i = 
+      if i == n then c else match s.[i] with
+	| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
+	| ' ' -> count (c + 1) (i + 1)
+	| _ -> c
+    in
+    count 0 0
+
+  let count_dashes s =
+    let c = ref 0 in
+    for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
+    !c
+
+  let cut_head_tail_spaces s =
+    let n = String.length s in
+    let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
+    let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
+    let l = look_up 0 in
+    let r = look_dn (n-1) in
+    if l <= r then String.sub s l (r-l+1) else s
+
+  let sec_title s =
+    let rec count lev i = 
+      if s.[i] = '*' then 
+	count (succ lev) (succ i) 
+      else 
+	let t = String.sub s i (String.length s - i) in
+	lev, cut_head_tail_spaces t
+    in
+    count 0 (String.index s '*')
+
+  let formatted = ref false
+  let brackets = ref 0
+
+  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 = {
+    st_gallina : bool;
+    st_light : bool
+  }
+
+  let state_stack = Stack.create ()
+
+  let save_state () = 
+    Stack.push { st_gallina = !gallina; st_light = !light } state_stack
+
+  let restore_state () =
+    let s = Stack.pop state_stack in
+    gallina := s.st_gallina;
+    light := s.st_light
+      
+  let without_ref r f x = save_state (); r := false; f x; restore_state ()
+
+  let without_gallina = without_ref gallina
+
+  let without_light = without_ref light
+
+  let show_all f = without_gallina (without_light f)
+
+  let begin_show () = save_state (); gallina := false; light := false
+  let end_show () = restore_state ()
+
+  (* Reset the globals *)
+
+  let reset () =
+    formatted := false;
+    brackets := 0;
+    gstate := AfterDot
+
+  (* erasing of Section/End *)
+
+  let section_re = Str.regexp "[ \t]*Section"
+  let end_re = Str.regexp "[ \t]*End"
+  let is_section s = Str.string_match section_re s 0
+  let is_end s = Str.string_match end_re s 0
+
+  let sections_to_close = ref 0
+
+  let section_or_end s =
+    if is_section s then begin
+      incr sections_to_close; true
+    end else if is_end s then begin
+      if !sections_to_close > 0 then begin 
+	decr sections_to_close; true 
+      end else 
+	false
+    end else
+      true
+
+  (* tokens pretty-print *)
+
+  let token_buffer = Buffer.create 1024
+
+  let token_re = 
+    Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
+  let printing_token_re =
+    Str.regexp
+      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
+
+  let add_printing_token toks pps =
+    try
+      if Str.string_match token_re toks 0 then
+	let tok = Str.matched_group 1 toks in
+	if Str.string_match printing_token_re pps 0 then
+	  let pp = 
+	    (try Some (Str.matched_group 3 pps) with _ -> 
+             try Some (Str.matched_group 4 pps) with _ -> None),
+	    (try Some (Str.matched_group 6 pps) with _ -> None)
+	  in
+	  Output.add_printing_token tok pp
+    with _ ->
+      ()
+
+  let remove_token_re = 
+    Str.regexp 
+      "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
+
+  let remove_printing_token toks =
+    try
+      if Str.string_match remove_token_re toks 0 then
+	let tok = Str.matched_group 1 toks in
+	Output.remove_printing_token tok
+    with _ ->
+      ()
+
+  let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
+  let extract_ident s =
+    assert (String.length s >= 3);
+    if Str.string_match extract_ident_re s 0 then
+      Str.matched_group 1 s
+    else
+      String.sub s 1 (String.length s - 3)
+
+}
+
+(*s Regular expressions *)
+
+let space = [' ' '\t']
+let space_nl = [' ' '\t' '\n' '\r']
+
+let firstchar = 
+  ['A'-'Z' 'a'-'z' '_' 
+  (* iso 8859-1 accents *) 
+  '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  (* utf-8 latin 1 supplement *) 
+  '\195' ['\128'-'\191'] |
+  (* utf-8 letterlike symbols *) 
+  '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+let identchar = 
+  firstchar | ['\'' '0'-'9' '@']
+let identifier = firstchar identchar*
+
+let symbolchar_no_brackets =
+  ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'
+   '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~'
+   '{' '}' '(' ')'] |
+  (* utf-8 symbols *) 
+  '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
+let symbolchar = symbolchar_no_brackets | '[' | ']'
+let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
+
+(* 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 = "    "
+
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* '\n'
+let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* '\n'
+let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* '\n'
+let end_show = "(*" space* "end" space+ "show" space* "*)" space* '\n'
+(*
+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'+
+      { 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 }
+  | space* "Comments" space_nl
+      { end_coq (); start_doc (); comments lexbuf; end_doc (); 
+	start_coq (); coq lexbuf }
+  | space* begin_hide
+      { skip_hide lexbuf; coq_bol lexbuf }
+  | space* begin_show
+      { begin_show (); coq_bol lexbuf }
+  | space* end_show
+      { end_show (); coq_bol lexbuf }
+  | space* coq_command_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 }
+  | 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 }
+  | 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* "*)"
+      { remove_printing_token (lexeme lexbuf);
+	coq_bol lexbuf }
+  | space* "(**" space+ "remove" space+ "printing" space+
+      { eprintf "warning: bad 'remove printing' command at character %d\n" 
+	  (lexeme_start lexbuf); flush stderr;
+	ignore (comment lexbuf);
+	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 }
+  | eof 
+      { () }
+  | _ 
+      { backtrack lexbuf; indentation 0; coq lexbuf }
+
+(*s Scanning Coq elsewhere *)
+
+and coq = parse
+  | "\n" 
+      { 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 }
+  | "(*"
+      { let eol = comment lexbuf in
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | '\n'+ space* "]]"
+      { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
+  | eof 
+      { () }
+  | token
+      { 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 }
+
+(*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*
+      { start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+  | eof 
+      { false }
+  | _ 
+      { backtrack lexbuf; doc lexbuf }
+
+(*s Scanning documentation elsewhere *)
+
+and doc = parse
+  | "\n"
+      { char '\n'; doc_bol lexbuf }
+  | "["
+      { brackets := 1; 
+	start_inline_coq (); escaped_coq lexbuf; end_inline_coq ();
+	doc lexbuf }
+  | "[[" '\n' space*
+      { formatted := true; start_code ();
+	indentation (count_spaces (lexeme lexbuf)); 
+	without_gallina coq lexbuf; 
+	end_code (); formatted := false;
+	doc lexbuf }
+  | '*'* "*)" space* '\n'
+      { true }
+  | '*'* "*)"
+      { false }
+  | "$"
+      { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
+  | "$$"
+      { char '$'; doc lexbuf }
+  | "%"
+      { escaped_latex lexbuf; doc lexbuf }
+  | "%%"
+      { char '%'; doc lexbuf }
+  | "#"
+      { escaped_html lexbuf; doc lexbuf }
+  | "##"
+      { char '#'; doc lexbuf }
+  | eof 
+      { false }
+  | _ 
+      { char (lexeme_char lexbuf 0); doc lexbuf }
+
+(*s Various escapings *)
+
+and escaped_math_latex = parse
+  | "$" { stop_latex_math () }
+  | eof { stop_latex_math () }
+  | _   { latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
+
+and escaped_latex = parse
+  | "%" { () }
+  | eof { () }
+  | _   { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
+
+and escaped_html = parse
+  | "#" { () }
+  | "&#"
+        { html_char '&'; html_char '#'; escaped_html lexbuf }
+  | "##"
+        { html_char '#'; escaped_html lexbuf }
+  | eof { () }
+  | _   { html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
+
+and verbatim = parse
+  | "\n>>" { verbatim_char '\n'; stop_verbatim () }
+  | eof { stop_verbatim () }
+  | _ { verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+
+(*s Coq, inside quotations *)
+
+and escaped_coq = parse
+  | "]"
+      { decr brackets; 
+	if !brackets > 0 then begin char ']'; escaped_coq lexbuf end }
+  | "["
+      { incr brackets; char '['; escaped_coq lexbuf }
+  | "(*"
+      { ignore (comment lexbuf); escaped_coq lexbuf }
+  | "*)"
+      { (* likely to be a syntax error: we escape *) backtrack lexbuf }
+  | eof
+      { () }
+  | token_brackets
+      { let s = lexeme lexbuf in
+	symbol s;
+	escaped_coq lexbuf }
+  | (identifier '.')* identifier
+      { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
+  | _ 
+      { char (lexeme_char lexbuf 0); escaped_coq lexbuf }
+
+(*s Coq "Comments" command. *)
+
+and comments = parse
+  | space_nl+ 
+      { char ' '; comments lexbuf }
+  | '"' [^ '"']* '"' 
+      { let s = lexeme lexbuf in
+	let s = String.sub s 1 (String.length s - 2) in
+	ignore (doc (from_string s)); comments lexbuf }
+  | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
+      { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
+  | "." (space_nl | eof)
+      { () }
+  | eof 
+      { () }
+  | _   
+      { char (lexeme_char lexbuf 0); comments lexbuf }
+
+(*s Skip comments *)
+
+and comment = parse
+  | "(*" { ignore (comment lexbuf); comment lexbuf }
+  | "*)" space* '\n'+ { true }
+  | "*)" { false }
+  | 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 }
+  | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
+  | _ { skip_to_dot lexbuf }
+
+and skip_hide = parse
+  | eof | end_hide { () }
+  | _ { skip_hide lexbuf }
+
+(*s Reading token pretty-print *)
+
+and printing_token = parse
+  | "*)" | eof 
+	{ let s = Buffer.contents token_buffer in 
+	  Buffer.clear token_buffer;
+	  s }
+  | _   { Buffer.add_string token_buffer (lexeme lexbuf); 
+	  printing_token lexbuf }
+
+(*s Applying the scanners to files *)
+
+{
+
+  type file =
+    | Vernac_file of string * coq_module
+    | Latex_file of string
+
+  let coq_file f m =
+    reset ();
+    Index.scan_file f m;
+    start_module ();
+    let c = open_in f in
+    let lb = from_channel c in
+    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/coqdoc/style.css b/tools/coqdoc/style.css
new file mode 100644
index 00000000..5150bd75
--- /dev/null
+++ b/tools/coqdoc/style.css
@@ -0,0 +1,23 @@
+a:visited {color : #416DFF; text-decoration : none; }
+a:link {color : #416DFF; text-decoration : none; font-weight : bold}
+a:hover {color : Red; text-decoration : underline; }
+a:active {color : Red; text-decoration : underline; }
+.keyword { font-weight : bold ; color : Red }
+.keywordsign { color : #C04600 }
+.superscript { font-size : 4 }
+.subscript { font-size : 4 }
+.comment { color : Green }
+.constructor { color : Blue }
+.string { color : Maroon }
+.warning { color : Red ; font-weight : bold }
+.info { margin-left : 3em; margin-right : 3em }
+.title1 { font-size : 20pt ; background-color : #416DFF }
+.title2 { font-size : 20pt ; background-color : #418DFF }
+.title3 { font-size : 20pt ; background-color : #41ADFF }
+.title4 { font-size : 20pt ; background-color : #41CDFF }
+.title5 { font-size : 20pt ; background-color : #41EDFF }
+.title6 { font-size : 20pt ; background-color : #41FFFF }
+body { background-color : White }
+tr { background-color : White }
+# .doc { background-color :#aaeeff  }
+.doc { background-color :#66ff66  }
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
new file mode 100644
index 00000000..08bf2bcc
--- /dev/null
+++ b/tools/coqwc.mll
@@ -0,0 +1,293 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* 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*)
+
+(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source. 
+    It assumes the files to be lexically well-formed. *)
+
+(*i*){ 
+open Printf
+open Lexing
+open Filename
+(*i*)
+
+(*s Command-line options. *)
+
+let spec_only = ref false
+let proof_only = ref false
+let percentage = ref false
+let skip_header = ref true
+
+(*s Counters. [clines] counts the number of code lines of the current
+    file, and [dlines] the number of comment lines. [tclines] and [tdlines]
+    are the corresponding totals. *)
+
+let slines = ref 0
+let plines = ref 0
+let dlines = ref 0
+
+let tslines = ref 0
+let tplines = ref 0
+let tdlines = ref 0
+
+let update_totals () =
+  tslines := !tslines + !slines; 
+  tplines := !tplines + !plines; 
+  tdlines := !tdlines + !dlines
+
+(*s The following booleans indicate whether we have seen spec, proof or
+    comment so far on the current line; when a newline is reached, [newline]
+    is called and updates the counters accordingly. *)
+
+let seen_spec = ref false
+let seen_proof = ref false
+let seen_comment = ref false
+
+let newline () =
+  if !seen_spec then incr slines; 
+  if !seen_proof then incr plines; 
+  if !seen_comment then incr dlines; 
+  seen_spec := false; seen_proof := false; seen_comment := false
+
+let reset_counters () = 
+  seen_spec := false; seen_proof := false; seen_comment := false;
+  slines := 0; plines := 0; dlines := 0
+
+(*s Print results. *)
+
+let print_line sl pl dl fo =
+  if not !proof_only then printf " %8d" sl;
+  if not !spec_only then printf " %8d" pl;
+  if not (!proof_only || !spec_only) then printf " %8d" dl;
+  (match fo with Some f -> printf " %s" f | _ -> ());
+  if !percentage then begin
+    let s = sl + pl + dl in
+    let p = if s > 0 then 100 * dl / s else 0 in
+    printf " (%d%%)" p
+  end;
+  print_newline ()
+
+let print_file fo = print_line !slines !plines !dlines fo
+
+let print_totals () = print_line !tslines !tplines !tdlines (Some "total")
+
+(*i*)}(*i*)
+
+(*s Shortcuts for regular expressions. The [rcs] regular expression
+    is used to skip the CVS infos possibly contained in some comments, 
+    in order not to consider it as documentation. *)
+
+let space = [' ' '\t' '\r']
+let character =
+  "'" ([^ '\\' '\''] |
+       '\\' (['\\' '\'' 'n' 't' 'b' 'r'] | ['0'-'9'] ['0'-'9'] ['0'-'9'])) "'"
+let rcs_keyword =
+  "Author" | "Date" | "Header" | "Id" | "Name" | "Locker" | "Log" |
+  "RCSfile" | "Revision" | "Source" | "State"
+let rcs = "\036" rcs_keyword [^ '$']* "\036"
+let stars = "(*" '*'* "*)"
+let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
+let proof_start =   
+  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness"
+let proof_end =
+  ("Save" | "Qed" | "Defined" | "Abort") [^'.']* '.'
+
+(*s [spec] scans the specification. *)
+
+rule spec = parse
+  | "(*"   { comment lexbuf; spec lexbuf }
+  | '"'    { let n = string lexbuf in slines := !slines + n; 
+	     seen_spec := true; spec lexbuf }
+  | '\n'   { newline (); spec lexbuf }
+  | space+ | stars 
+           { spec lexbuf }
+  | proof_start space
+           { seen_spec := true; spec_to_dot lexbuf; proof lexbuf }
+  | proof_start '\n'
+           { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf }
+  | "Definition" space
+           { seen_spec := true; definition lexbuf }
+  | character | _ 
+	   { seen_spec := true; spec lexbuf }
+  | eof    { () }
+
+(*s [spec_to_dot] scans a spec until a dot is reached and returns. *)
+
+and spec_to_dot = parse
+  | "(*"   { comment lexbuf; spec_to_dot lexbuf }
+  | '"'    { let n = string lexbuf in slines := !slines + n; 
+	     seen_spec := true; spec_to_dot lexbuf }
+  | '\n'   { newline (); spec_to_dot lexbuf }
+  | dot    { () }
+  | space+ | stars 
+           { spec_to_dot lexbuf }
+  | character | _ 
+	   { seen_spec := true; spec_to_dot lexbuf }
+  | eof    { () }
+
+(*s [definition] scans a definition; passes to [proof] is the body is 
+    absent, and to [spec] otherwise *)
+
+and definition = parse
+  | "(*"   { comment lexbuf; definition lexbuf }
+  | '"'    { let n = string lexbuf in slines := !slines + n; 
+	     seen_spec := true; definition lexbuf }
+  | '\n'   { newline (); definition lexbuf }
+  | ":="   { seen_spec := true; spec lexbuf }
+  | dot    { proof lexbuf }
+  | space+ | stars 
+           { definition lexbuf }
+  | character | _ 
+	   { seen_spec := true; definition lexbuf }
+  | eof    { () }
+
+(*s Scans a proof, then returns to [spec]. *)
+
+and proof = parse
+  | "(*"   { comment lexbuf; proof lexbuf }
+  | '"'    { let n = string lexbuf in plines := !plines + n; 
+	     seen_proof := true; proof lexbuf }
+  | space+ | stars 
+           { proof lexbuf }
+  | '\n'   { newline (); proof lexbuf }
+  | "Proof" space* '.' 
+           { seen_proof := true; proof lexbuf }
+  | "Proof" space
+           { proof_term lexbuf }
+  | proof_end
+           { seen_proof := true; spec lexbuf }
+  | character | _ 
+	   { seen_proof := true; proof lexbuf }
+  | eof    { () }
+
+and proof_term = parse
+  | "(*"   { comment lexbuf; proof_term lexbuf }
+  | '"'    { let n = string lexbuf in plines := !plines + n; 
+	     seen_proof := true; proof_term lexbuf }
+  | space+ | stars 
+           { proof_term lexbuf }
+  | '\n'   { newline (); proof_term lexbuf }
+  | dot    { spec lexbuf }
+  | character | _ 
+	   { seen_proof := true; proof_term lexbuf }
+  | eof    { () }
+
+(*s Scans a comment. *)
+
+and comment = parse
+  | "(*"   { comment lexbuf; comment lexbuf }
+  | "*)"   { () }
+  | '"'    { let n = string lexbuf in dlines := !dlines + n; 
+	     seen_comment := true; comment lexbuf }
+  | '\n'   { newline (); comment lexbuf }
+  | space+ | stars
+	   { comment lexbuf }
+  | character | _ 
+	   { seen_comment := true; comment lexbuf }
+  | eof    { () }
+
+(*s The entry [string] reads a string until its end and returns the number
+    of newlines it contains. *)
+
+and string = parse
+  | '"'  { 0 }
+  | '\\' ('\\' | 'n' | '"') { string lexbuf }
+  | '\n' { succ (string lexbuf) }
+  | _    { string lexbuf }
+  | eof  { 0 }
+
+(*s The following entry [read_header] is used to skip the possible header at
+    the beggining of files (unless option \texttt{-e} is specified).
+    It stops whenever it encounters an empty line or any character outside
+    a comment. In this last case, it correctly resets the lexer position
+    on that character (decreasing [lex_curr_pos] by 1). *)
+ 
+and read_header = parse
+  | "(*"   { skip_comment lexbuf; skip_until_nl lexbuf; 
+	     read_header lexbuf }
+  | "\n"   { () }
+  | space+ { read_header lexbuf }
+  | _      { lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos - 1 }
+  | eof    { () }
+
+and skip_comment = parse
+  | "*)" { () }
+  | "(*" { skip_comment lexbuf; skip_comment lexbuf }
+  | _    { skip_comment lexbuf }
+  | eof  { () }
+
+and skip_until_nl = parse
+  | '\n' { () }
+  | _    { skip_until_nl lexbuf }
+  | eof  { () }
+
+(*i*){(*i*)
+
+(*s Processing files and channels. *)
+
+let process_channel ch =
+  let lb = Lexing.from_channel ch in
+  reset_counters ();
+  if !skip_header then read_header lb;
+  spec lb
+
+let process_file f =
+  try
+    let ch = open_in f in
+    process_channel ch;
+    close_in ch;
+    print_file (Some f);
+    update_totals ()
+  with
+    | Sys_error "Is a directory" -> 
+	flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
+    | Sys_error s -> 
+	flush stdout; eprintf "coqwc: %s\n" s; flush stderr
+
+(*s Parsing of the command line. *)
+
+let usage () =
+  prerr_endline "usage: coqwc [options] [files]";
+  prerr_endline "Options are:";
+  prerr_endline "  -p   print percentage of comments";
+  prerr_endline "  -s   print only the spec size";
+  prerr_endline "  -r   print only the proof size";
+  prerr_endline "  -e   (everything) do not skip headers";
+  exit 1
+
+let rec parse = function
+  | [] -> []
+  | ("-h" | "-?" | "-help" | "--help") :: _ -> usage ()
+  | ("-s" | "--spec-only") :: args -> 
+      proof_only := false; spec_only := true; parse args
+  | ("-r" | "--proof-only") :: args -> 
+      spec_only := false; proof_only := true; parse args
+  | ("-p" | "--percentage") :: args -> percentage := true; parse args
+  | ("-e" | "--header") :: args -> skip_header := false; parse args
+  | f :: args -> f :: (parse args)
+
+(*s Main program. *)
+
+let main () =
+  let files = parse (List.tl (Array.to_list Sys.argv)) in
+  if not (!spec_only || !proof_only) then 
+    printf "     spec    proof comments\n";
+  match files with
+    | [] -> process_channel stdin; print_file None
+    | [f] -> process_file f
+    | _ -> List.iter process_file files; print_totals ()
+
+let _ = Printexc.catch main ()
+
+(*i*)}(*i*)
+
+
diff --git a/tools/gallina.ml b/tools/gallina.ml
new file mode 100644
index 00000000..c997820c
--- /dev/null
+++ b/tools/gallina.ml
@@ -0,0 +1,66 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: gallina.ml,v 1.2.16.1 2004/07/16 19:31:46 herbelin Exp $ *)
+
+open Gallina_lexer
+
+let vfiles = ref ([] : string list)
+
+let option_moins = ref false
+
+let option_stdout = ref false
+
+let traite_fichier f = 
+  try 
+    let chan_in = open_in (f^".v") in 
+    let buf = Lexing.from_channel chan_in in
+    if not !option_stdout then chan_out := open_out (f ^ ".g");
+    try 
+      while true do Gallina_lexer.action buf done
+    with Fin_fichier -> begin 
+      flush !chan_out;
+      close_in chan_in;
+      if not !option_stdout then close_out !chan_out
+    end
+  with Sys_error _ -> 
+    () 
+
+let traite_stdin () =
+  try
+    let buf = Lexing.from_channel stdin in
+    try 
+      while true do Gallina_lexer.action buf done
+    with Fin_fichier -> 
+      flush !chan_out
+  with Sys_error _ -> 
+    ()
+
+let gallina () =
+  let lg_command = Array.length Sys.argv in
+  if lg_command < 2 then begin
+    output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
+    flush stderr;
+    exit 1
+  end;
+  let treat = function
+    | "-" -> option_moins := true
+    | "-stdout" -> option_stdout := true
+    | "-nocomments" -> comments := false
+    | f -> 
+	if Filename.check_suffix f ".v" then
+       	  vfiles := (Filename.chop_suffix f ".v") :: !vfiles
+  in
+  Array.iter treat Sys.argv;
+  if !option_moins then
+    traite_stdin ()
+  else
+    List.iter traite_fichier !vfiles
+
+let _ = Printexc.catch gallina ()
+
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
new file mode 100644
index 00000000..ce9fb950
--- /dev/null
+++ b/tools/gallina_lexer.mll
@@ -0,0 +1,128 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: gallina_lexer.mll,v 1.5.6.1 2004/07/16 19:31:46 herbelin Exp $ *)
+
+{
+ open Lexing
+
+ let chan_out = ref stdout
+
+ let comment_depth = ref 0
+ let cRcpt = ref 0
+ let comments = ref true
+ let print s = output_string !chan_out s
+ 
+ exception Fin_fichier
+
+}
+
+let space = [' ' '\t' '\n' '\r']
+let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
+
+rule action = parse
+  | "Theorem" space { print "Theorem "; body lexbuf; 
+  	              cRcpt := 1; action lexbuf }
+  | "Lemma" space   { print "Lemma ";   body lexbuf; 
+      	       	      cRcpt := 1; action lexbuf }
+  | "Fact" space    { print "Fact ";   body lexbuf; 
+      	       	      cRcpt := 1; action lexbuf }
+  | "Remark" space  { print "Remark ";  body lexbuf; 
+      	       	      cRcpt := 1; action lexbuf }
+  | "Goal" space    { print "Goal ";    body lexbuf; 
+      	       	      cRcpt := 1; action lexbuf }
+  | "Correctness" space { print "Correctness "; body_pgm lexbuf; 
+      	       	          cRcpt := 1; action lexbuf }
+  | "Definition" space  { print "Definition "; body_def lexbuf;
+			  cRcpt := 1; action lexbuf }
+  | "Hint" space        { skip_until_point lexbuf ; action lexbuf }
+  | "Hints" space        { skip_until_point lexbuf ; action lexbuf }
+  | "Transparent" space { skip_until_point lexbuf ; action lexbuf }
+  | "Immediate"	space   { skip_until_point lexbuf ; action lexbuf }
+  | "Syntax" space      { skip_until_point lexbuf ; action lexbuf }
+  | "(*"      { (if !comments then print "(*");
+		comment_depth := 1;
+      	        comment lexbuf;
+		cRcpt := 0; action lexbuf }
+  | [' ' '\t']* '\n'      { if !cRcpt < 2 then print "\n";
+      	       	       	    cRcpt := !cRcpt+1; action lexbuf}
+  | eof       { raise Fin_fichier}
+  | _         { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
+
+and comment = parse
+  | "(*"  { (if !comments then print "(*"); 
+      	    comment_depth := succ !comment_depth; comment lexbuf }
+  | "*)"  { (if !comments then print "*)");
+      	    comment_depth := pred !comment_depth;
+            if !comment_depth > 0 then comment lexbuf }
+  | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf));
+      			  comment_depth := pred !comment_depth;
+			  if !comment_depth > 0 then comment lexbuf }
+  | eof   { raise Fin_fichier } 
+  | _     { (if !comments then print (Lexing.lexeme lexbuf)); 
+	    comment lexbuf }
+
+and skip_comment = parse
+  | "(*"  { comment_depth := succ !comment_depth; skip_comment lexbuf }
+  | "*)"  { comment_depth := pred !comment_depth;
+            if !comment_depth > 0 then skip_comment lexbuf }
+  | eof   { raise Fin_fichier } 
+  | _     { skip_comment lexbuf }
+
+and body_def = parse
+  | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () }
+  | _            { print (Lexing.lexeme lexbuf); body lexbuf }
+
+and body = parse
+  | enddot { print ".\n"; skip_proof lexbuf }
+  | ":="   { print ".\n"; skip_proof lexbuf }
+  | "(*"   { print "(*"; comment_depth := 1;
+      	     comment lexbuf; body lexbuf }
+  | eof    { raise Fin_fichier } 
+  | _      { print (Lexing.lexeme lexbuf); body lexbuf }
+
+and body_pgm = parse
+  | enddot { print ".\n"; skip_proof lexbuf }
+  | "(*"   { print "(*"; comment_depth := 1;
+      	     comment lexbuf; body_pgm lexbuf }
+  | eof    { raise Fin_fichier } 
+  | _      { print (Lexing.lexeme lexbuf); body_pgm lexbuf }
+
+and skip_until_point = parse
+  | '.' '\n' { () }
+  | enddot   { end_of_line lexbuf }
+  | "(*"     { comment_depth := 1;
+      	       skip_comment lexbuf; skip_until_point lexbuf }
+  | eof      { raise Fin_fichier } 
+  | _        { skip_until_point lexbuf }
+
+and end_of_line = parse
+  | [' ' '\t' ]*	{ end_of_line lexbuf }
+  | '\n'		{ () }
+  | eof   	     	{ raise Fin_fichier } 
+  | _	  		{ print (Lexing.lexeme lexbuf) }
+
+and skip_proof = parse
+  | "Save."	{ end_of_line lexbuf }
+  | "Save" space
+                { skip_until_point lexbuf }
+  | "Qed."  	{ end_of_line lexbuf }
+  | "Qed" space
+                { skip_until_point lexbuf }
+  | "Defined."  { end_of_line lexbuf }
+  | "Defined" space
+                { skip_until_point lexbuf }
+  | "Abort." 	{ end_of_line lexbuf }
+  | "Abort" space
+                { skip_until_point lexbuf }
+  | "Proof" space   { skip_until_point lexbuf }
+  | "Proof" [' ' '\t']* '.'  { skip_proof lexbuf }
+  | "(*"    { comment_depth := 1;
+      	      skip_comment lexbuf; skip_proof lexbuf }
+  | eof     { raise Fin_fichier } 
+  | _       { skip_proof lexbuf }
diff --git a/tools/restore-v7 b/tools/restore-v7
new file mode 100755
index 00000000..ab884587
--- /dev/null
+++ b/tools/restore-v7
@@ -0,0 +1,9 @@
+#!/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
new file mode 100755
index 00000000..7d71bea9
--- /dev/null
+++ b/tools/translate-v8
@@ -0,0 +1,41 @@
+#!/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
new file mode 100755
index 00000000..10e7f140
--- /dev/null
+++ b/tools/translate_V6-3-1_to_V7-0
@@ -0,0 +1,27 @@
+#! /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
new file mode 100755
index 00000000..36d0bf8c
--- /dev/null
+++ b/tools/upgrade-v8
@@ -0,0 +1,22 @@
+#!/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