outils (manquent encore les deux filtres)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@235 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 2083 insertions, 0 deletions

diff --git a/tools/.cvsignore b/tools/.cvsignore
new file mode 100644
index 000000000..4e765a8af
--- /dev/null
+++ b/tools/.cvsignore
@@ -0,0 +1,6 @@
+coqdep_lexer.ml
+gallina_lexer.ml
+coqdep
+coq_makefile
+gallina
+coq-tex
diff --git a/tools/README.coq-tex b/tools/README.coq-tex
new file mode 100755
index 000000000..5c7606a96
--- /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 000000000..0d27b607f
--- /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/coq-sl.sty b/tools/coq-sl.sty
new file mode 100755
index 000000000..9f6e5480c
--- /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.1 b/tools/coq-tex.1
new file mode 100755
index 000000000..737de70a9
--- /dev/null
+++ b/tools/coq-tex.1
@@ -0,0 +1,125 @@
+.TH COQ-TEX 1 "29 March 1995"
+
+.SH NAME
+coq-tex \- Process Coq phrases embedded in LaTeX files
+
+.SH SYNOPSIS
+.B coq-tex
+[
+.BI \-o \ output-file
+]
+[
+.BI \-n \ line-width
+]
+[
+.BI \-image \ coq-image
+]
+[
+.B -w
+]
+[
+.B -v
+]
+[
+.B -sl
+]
+[
+.B -hrule
+]
+[
+.B -small
+]
+.I input-file ...
+
+
+.SH DESCRIPTION
+
+The
+.B coq-tex
+filter extracts Coq phrases embedded in LaTeX files, evaluates
+them, and insert the outcome of the evaluation after each phrase.
+
+Three LaTeX environments are provided to include Coq code in
+the input files:
+.TP
+.B coq_example
+The phrases between \\begin{coq_example} and \\end{coq_example} are
+evaluated and copied into the output file. Each phrase is followed by
+the response of the toplevel loop.
+.TP
+.B coq_example*
+The phrases between \\begin{coq_example*} and \\end{coq_example*} are
+evaluated and copied into the output file. The responses of the
+toplevel loop are discarded.
+.TP
+.B coq_eval
+The phrases between \\begin{coq_eval} and \\end{coq_eval} are
+silently evaluated. They are not copied into the output file, and the
+responses of the toplevel loop are discarded.
+.PP
+The resulting LaTeX code is stored in the file
+.IR file \&.v.tex
+if the input file has a name of the form
+.IR file \&.tex,
+otherwise the name of the output file is the name of the input file
+with `.v.tex' appended.
+
+The files produced by
+.B coq-tex
+can be directly processed by LaTeX. 
+Both the Coq phrases and the toplevel output are typeset in
+typewriter font.
+
+.SH OPTIONS
+
+.TP
+.BI \-o \ output-file
+Specify the name of a file where the LaTeX output is to be stored. A
+dash `-' causes the LaTeX output to be printed on standard output.
+.TP
+.BI \-n \ line-width
+Set the line width. The default is 72 characters. The responses of the
+toplevel loop are folded if they are longer than the line width. No
+folding is performed on the Coq input text.
+.TP
+.BI \-image \ coq-image
+Cause the file
+.IR coq-image
+to be executed to evaluate the Coq phrases. By default,
+this is the command 
+.IR coqtop
+without specifying any path which is used to evaluate the Coq phrases.
+.TP
+.B -w
+Cause lines to be folded on a space character whenever possible,
+avoiding word cuts in the output. By default, folding occurs at
+the line width, regardless of word cuts.
+.TP
+.B -v
+Verbose mode. Prints the Coq answers on the standard output.
+Useful to detect errors in Coq phrases.
+.TP
+.B -sl
+Slanted mode. The Coq answers are written in a slanted font.
+.TP
+.B -hrule
+Horizontal lines mode. The Coq parts are written between two
+horizontal lines.
+.TP
+.B -small
+Small font mode. The Coq parts are written in a smaller font.
+
+
+.SH CAVEATS
+The \\begin... and \\end... phrases must sit on a line by themselves,
+with no characters before the backslash or after the closing brace.
+Each Coq phrase must be terminated by `.' at the end of a line.
+Blank space is accepted between `.' and the newline, but any other
+character will cause coq-tex to ignore the end of the phrase,
+resulting in an incorrect shuffling of the responses into the phrases.
+(The responses ``lag behind''.)
+
+.SH SEE ALSO
+
+.B coqtop
+(1).
diff --git a/tools/coq-tex.ml b/tools/coq-tex.ml
new file mode 100644
index 000000000..69882c0ce
--- /dev/null
+++ b/tools/coq-tex.ml
@@ -0,0 +1,264 @@
+
+(* $Id$ *)
+
+(* 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\*\|eval\)}[ \t]*$"
+let end_coq   = Str.regexp "\\\\end{coq_\(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
+    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\*\)}[ \t]*$"
+let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
+let end_coq_example = Str.regexp "\\\\end{coq_\(example\|example\*\)}[ \t]*$"
+let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
+let dot_end_line = Str.regexp "\\.[ \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 outside of a \begin{coq_...} ... \end{coq_...} block *)
+  let rec 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") 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 k first_block = 
+    let s = input_line c_tex in
+    if Str.string_match end_coq_example s 0 then 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";
+      outside ()
+    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";
+      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 0 false
+      end else
+	inside show_answers (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 *)
+    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 000000000..d54c888f5
--- /dev/null
+++ b/tools/coq.el
@@ -0,0 +1,176 @@
+;; coq.el --- Coq mode editing commands for Emacs
+
+;; Jean-Christophe Filliatre, march 1995
+;; Honteusement pompé de caml.el, Xavier Leroy, july 1993.
+
+(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)
+)
+
+(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.")
+
+;;; 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)
+  (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)
+  (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)
\ No newline at end of file
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
new file mode 100644
index 000000000..288d8a035
--- /dev/null
+++ b/tools/coq_makefile.ml
@@ -0,0 +1,385 @@
+
+(* $Id$ *)
+
+(* 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
+
+let output_channel = ref stdout
+
+let some_file = ref false
+
+let some_vfile = ref false
+
+let some_mlfile = ref false
+
+let opt = ref "-opt"
+
+let print x = output_string !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:
+
+do_Makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
+  command dependencies file] ... [-I dir] ... [VARIABLE = value] ...
+  [-full] [-no-opt] [-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\"
+[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
+[-full]: \"opt\" should use \"coqc -full\" instead of \"coqc -opt\"
+[-no-opt]: target \"opt\" should be equivalent to \"byte\"
+[-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::\n";
+  if !some_file then begin
+    print "\trm .depend\n";
+    print "\t$(COQDEP) -i $(LIBS) *.v *.ml *.mli >.depend\n";
+    print "\t$(COQDEP) $(LIBS) -suffix .html *.v >>.depend\n";
+    if !some_mlfile then print "\t$(P4DEP) *.ml >>.depend\n"
+  end;
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n")
+    sds;
+  print "\n";
+  print "install::\n";
+  print "\t@if test -z $(TARGETDIR); then echo \"You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')\"; exit 1; fi\n";
+  if !some_vfile then print "\tcp -f *.vo $(TARGETDIR)\n";
+  if !some_mlfile then print "\tcp -f *.cmo $(TARGETDIR)\n";
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n")
+    sds;
+  print "\n";
+  print "Makefile::\n";
+  print "\tmv -f Makefile Makefile.bak\n";
+  print "\tdo_Makefile -f Make -o Makefile\n";
+  print "\n";
+  print "clean::\n";
+  print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~\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"
+
+let implicit () =
+  let ml_rules () =
+    print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n" ;
+    print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n" ;
+    print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n" ;
+    print ".ml4.cmo:\n\t$(CAMLC) -pp $(P4) $(ZDEBUG) $(ZFLAGS) -impl $<\n\n";
+    print ".ml4.cmx:\n\t$(CAMLOPTC) -pp $(P4) $(ZDEBUG) $(ZFLAGS)\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.html:\n\t$(COQ2HTML) $<\n\n" ;
+    print ".v.tex:\n\t$(COQ2LATEX) $< -latex -o $@\n\n" ;
+    print ".v.g.html:\n\t$(GALLINA) -stdout $< | $(COQ2HTML) -f > $@\n\n" ;
+    print 
+      ".v.g.tex:\n\t$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -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)/src/tactics -I $(COQTOP)/src/proofs \\
+  -I $(COQTOP)/src/syntax -I $(COQTOP)/src/env -I $(COQTOP)/src/lib/util \\
+  -I $(COQTOP)/src/constr -I $(COQTOP)/tactics -I $(COQTOP)/src/meta \\
+  -I $(COQTOP)/src/parsing -I $(COQTOP)/src/typing -I $(CAMLP4LIB)\n";
+  print "ZFLAGS=$(LIBS) $(COQSRC)\n";
+  print "FULLOPT=$(OPT:-opt=-full)\n";
+  if !opt="-opt" then
+    print "COQFLAGS=-q $(OPT) $(LIBS)\n"
+  else begin
+    print "OPTCOQ=";
+    print "$(OPT:-opt="; print !opt; print ")\n";
+    print "COQFLAGS=-q $(OPTCOQ) $(LIBS)\n"
+  end;
+  print "COQC=$(COQBIN)coqc\n";
+  print "COQFULL=$(COQBIN)coqc $(FULLOPT) -q $(LIBS)\n";
+  print "GALLINA=gallina\n";
+  print "COQ2HTML=coq2html\n";
+  print "COQ2LATEX=coq2latex\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 "P4=$(COQBIN)call_camlp4 -I $(COQTOP)/src/parsing \\
+  -I $(COQTOP)/theories/INIT -I $(COQTOP)/tactics\n";
+  print "P4DEP=$(COQBIN)camlp4dep\n";
+  var_aux l;
+  print "\n"
+
+let include_dirs l =
+  let rec include_aux = function
+    | [] -> []
+    | Include x :: r -> ("-I "^x) :: (include_aux r)
+    | _ :: r -> include_aux r
+  in
+  let i = "-I ." :: (include_aux l) in
+  if i <> [] then begin
+    section "Libraries definition.";
+    print "LIBS="; print_list "\\\n  " i; print "\n\n"
+  end
+
+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,dependencies,com)::r -> (file,dependencies,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"::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 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 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
+    | Def _ :: r -> fnames r
+    | [] -> []
+  in
+  section "Definition of the \"all\" target.";
+  print "all:: "; print_list "\\\n  " (fnames l) ;
+  print "\n\n" ;
+  if !some_vfile then begin
+    print "spec:: "; print_list "\\\n  " (vifiles l) ;
+    print "\n\n";
+    print "gallina:: "; print_list "\\\n  " (gfiles l) ;
+    print "\n\n";
+    print "html:: "; print_list "\\\n  " (hfiles l) ;
+    print "\n\n";
+    print "tex:: "; print_list "\\\n  " (tfiles l) ;
+    print "\n\n";
+    print "gallinatex:: "; print_list "\\\n  " (gtfiles l) ;
+    print "\n\n";
+    print "gallinahtml:: "; print_list "\\\n  " (ghfiles l) ;
+    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" :: r -> 
+      opt := "" ; process_cmd_line r
+  | "-full"::r -> 
+      opt := "-full" ; 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)
+  | ("-I" | "-h" | "--help" | "-custom") :: _ -> 
+      usage ()
+  | "-f"::file::r -> 
+      process_cmd_line ((parse file)@r)
+  | ["-f"] -> 
+      usage ()
+  | "-o" :: file :: r -> 
+      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 V6.1                                  ##
+##                                                                          ##
+##                                                                          ##
+##############################################################################
+
+"
+
+let warning () =
+  print "# WARNING\n#\n";
+  print "# This Makefile has been automagically generated by do_Makefile\n";
+  print "# Edit at your own risks !\n";
+  print "#\n# END OF WARNING\n\n"
+
+let command_line args =
+  print "#\n# This Makefile was generated by the command line :\n";
+  print "# do_Makefile ";
+  List.iter (fun x -> print x; print " ") args;
+  print "\n#\n\n"
+
+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;
+  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.1 b/tools/coqdep.1
new file mode 100755
index 000000000..342a52d66
--- /dev/null
+++ b/tools/coqdep.1
@@ -0,0 +1,182 @@
+.TH COQ 1 "28 March 1995" "Coq tools"
+
+.SH NAME
+coqdep \- Compute inter-module dependencies for Coq and Caml programs
+
+.SH SYNOPSIS
+.B coqdep
+[
+.BI \-w
+]
+[
+.BI \-I \ directory
+]
+[
+.BI \-coqlib \ directory
+]
+[
+.BI \-c
+]
+[
+.BI \-i
+]
+[
+.BI \-D
+]
+.I filename ...
+.I directory ...
+
+.SH DESCRIPTION
+
+.B coqdep
+compute inter-module dependencies for Coq and Caml programs,
+and prints the dependencies on the standard output in a format
+readable by make.
+When a directory is given as argument, it is recursively looked at.
+
+Dependencies of Coq modules are computed by looking at
+.IR Require \&
+commands (Require, Require Export, Require Import, Require Implementation),
+and
+.IR Declare \& 
+.IR ML \& 
+.IR Module \&
+commands. Dependencies relative to modules from the Coq library are not
+printed.
+
+Dependencies of Caml modules are computed by looking at
+.IR open \&
+directives and the dot notation
+.IR module.value \&.
+
+.SH OPTIONS
+
+.TP
+.BI \-c
+Prints the dependencies of Caml modules.
+(On Caml modules, the behaviour is exactly the same as cldepend,
+except that nested comments and strings are correctly handled).
+.TP
+.BI \-w
+Prints a warning if a Coq command
+.IR Declare \& 
+.IR ML \& 
+.IR Module \&
+is incorrect. (For instance, you wrote `Declare ML Module "A".',
+but the module A contains #open "B"). The correct command is printed
+(see option -D). The warning is printed on standard error.
+.TP
+.BI \-i
+Prints also the dependencies for .vi files (Coq specification modules).
+.TP
+.BI \-D
+This commands looks for every command
+.IR Declare \& 
+.IR ML \& 
+.IR Module \&
+of each Coq file given as argument and complete (if needed)
+the list of Caml modules. The new command is printed on
+the standard output. No dependency is computed with this option.
+.TP 
+.BI \-I \ directory
+The files .v .ml .mli of the directory
+.IR directory \&
+are taken into account during the calculus of dependencies,
+but their own dependencies are not printed.
+.TP 
+.BI \-coqlib \ directory
+Indicates where is the Coq library. The default value has been
+determined at installation time, and therefore this option should not
+be used.
+
+
+.SH SEE ALSO
+
+.BR camlc (1),
+.BR coqc (1),
+.BR make (1).
+.br
+
+.SH NOTES
+
+Lexers (for Coq and Caml) correctly handle nested comments
+and strings.
+
+The treatment of symbolic links is primitive.
+
+If two files have the same name, in two different directories,
+a warning is printed on standard error.
+
+There is no way to limit the scope of the recursive search for
+directories.
+
+.SH EXAMPLES
+
+.LP
+Consider the files (in the same directory):
+
+	A.ml B.ml C.ml D.ml X.v Y.v and Z.v
+
+where
+.TP
+.BI \+ 
+D.ml contains the commands `#open "A"', `#open "B"' and `type t = C__t' ;
+.TP
+.BI \+
+Y.v contains the command `Require X' ;
+.TP
+.BI \+
+Z.v contains the commands `Require X' and `Declare ML Module "D"'.
+.LP
+To get the dependencies of the Coq files:
+.IP
+.B
+example% coqdep -I . *.v
+.RS
+.sp .5
+.nf
+.B Z.vo: Z.v ./X.vo ./D.zo
+.B Y.vo: Y.v ./X.vo
+.B X.vo: X.v
+.fi
+.RE
+.br
+.ne 7
+.LP
+With a warning:
+.IP
+.B
+example% coqdep -w -I . *.v
+.RS
+.sp .5
+.nf
+.B Z.vo: Z.v ./X.vo ./D.zo
+.B Y.vo: Y.v ./X.vo
+.B X.vo: X.v
+### Warning : In file Z.v, the ML modules declaration should be
+### Declare ML Module "A" "B" "C" "D".
+.fi
+.RE
+.br
+.ne 7
+.LP
+To get only the Caml dependencies:
+.IP
+.B
+example% coqdep -c -I . *.ml
+.RS
+.sp .5
+.nf
+.B D.zo: D.ml ./A.zo ./B.zo ./C.zo
+.B C.zo: C.ml
+.B B.zo: B.ml
+.B A.zo: A.ml
+.fi
+.RE
+.br
+.ne 7
+
+.SH BUGS
+
+Please report any bug to
+.B coq@pauillac.inria.fr
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
new file mode 100755
index 000000000..16b0e4809
--- /dev/null
+++ b/tools/coqdep.ml
@@ -0,0 +1,414 @@
+
+(* $Id$ *)
+
+open Coqdep_lexer
+open Unix
+
+let stderr = Pervasives.stderr
+let stdout = Pervasives.stdout
+
+let option_c = ref false
+
+let option_D = ref false
+
+let option_w = ref false
+
+let option_i = ref false
+
+let suffixe = ref ".vo"
+let suffixe_spec = ref ".vi"
+
+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
+	  deja_vu := str :: !deja_vu;
+          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 warning_notfound f s =
+  output_string stderr ("*** Warning : in file " ^ f ^ ", the file ");
+  output_string stderr ( s ^ ".v is required and has not been found !\n");
+  flush stderr
+
+let traite_fichier_Coq f = 
+  try 
+    let chan = open_in f in 
+    let buf = Lexing.from_channel chan in 
+    let deja_vu_v = ref ([]: string 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
+	        deja_vu_v := str :: !deja_vu_v;
+                try
+                  let vdir = List.assoc str !vKnown in
+                  print_string " ";
+                  print_string (file_name (str,vdir));
+                  print_string (if spec then !suffixe_spec else !suffixe)
+                with Not_found -> 
+                  begin 
+		    try let _ = List.assoc str !coqlibKnown in ()
+                    with Not_found -> warning_notfound f str end
+       	      end
+	  | RequireString (spec,s) -> 
+	      let str = Filename.basename s in
+	      if not (List.mem str !deja_vu_v) then begin
+	        deja_vu_v := str :: !deja_vu_v;
+                try
+                  let vdir = List.assoc str !vKnown in
+                  print_string " ";
+                  print_string (file_name (str,vdir));
+                  print_string (if spec then !suffixe_spec else !suffixe)
+                with Not_found -> 
+                  begin try  let _ = List.assoc s !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
+		     deja_vu_ml := str :: !deja_vu_ml;
+               	     try
+              	       let mldir = List.assoc str !mlKnown in
+              	       print_string " ";
+                       print_string (file_name (str,mldir));
+              	       print_string ".cmo"
+              	     with Not_found -> () 
+		   end)
+		sl
+      done
+    with Fin_fichier -> ();
+      close_in chan
+  with Sys_error _ -> () 
+
+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
+	    output_string stderr ("*** Warning : in file "^f^" the");
+	    output_string stderr (" notation "^b^"__ is useless !\n");
+	    flush stderr
+	  end else if List.mem str !deja_vu then 
+	    ()
+	  else 
+	    deja_vu := str :: !deja_vu
+      	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 = 
+  print_newline ();
+  print_string ("*** In file "^f^" : ");
+  print_newline ();
+  print_string "Declare ML Module";
+  List.iter (fun str -> print_string " ";
+	       print_char '"'; print_string str;
+	       print_char '"') dcl;
+  print_string ".";
+  print_newline();
+  flush stdout
+
+let warning_Declare f dcl =
+  output_string stderr ("*** Warning : in file "^f^", the ML modules");
+  output_string stderr " declaration should be\n";
+  output_string stderr "*** Declare ML Module";
+  List.iter (fun str -> output_string stderr " ";
+	       output_char stderr '"'; output_string stderr str;
+	       output_char stderr '"') dcl;
+  output_string stderr ".\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 -> if f1 = f && d1 = d then true else 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
+       print_string fullname; print_string ".cmo: "; 
+       print_string fullname; print_string ext;
+       if file_mem pairname !mliAccu then begin
+	 print_string " "; print_string fullname; print_string ".cmi"
+       end;
+       print_string dep;
+       print_newline ();
+       print_string fullname; print_string ".cmx: "; 
+       print_string fullname; print_string ext;
+       if file_mem pairname !mliAccu then begin
+	 print_string " "; print_string fullname; print_string ".cmi"
+       end;
+       print_string dep_opt;
+       print_newline ();
+       flush stdout)
+    !mlAccu;
+  List.iter
+    (fun ((name,ext,dirname) as pairname) ->
+       let fullname = file_name (name,dirname) in
+       let (dep,_) = traite_fichier_ML fullname ext in
+       print_string fullname; print_string ".cmi: "; 
+       print_string fullname;print_string ext;
+       print_string dep;
+       print_newline ();
+       flush stdout)
+    !mliAccu
+
+let coq_dependencies () =
+  List.iter
+    (fun ((name,dirname) as pairname) ->
+       let fullname = file_name pairname in
+       Printf.printf "%s%s: %s.v" fullname !suffixe fullname;
+       traite_fichier_Coq (fullname^".v");
+       print_newline ();
+       if !option_i then begin
+	 Printf.printf "%s%s: %s.v" fullname !suffixe_spec fullname;
+	 traite_fichier_Coq (fullname^".v");
+	 print_newline ();
+       end;
+       flush stdout)
+    !vAccu
+
+let declare_dependencies () =
+  List.iter
+    (fun ((name,dirname) as pairname) ->
+       let fullname = file_name pairname in
+       traite_Declare (fullname^".v");      
+       flush stdout)
+    !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
+	     output_string stderr "*** Warning : the file ";
+	     output_string stderr (f ^ suf);
+	     output_string stderr " is defined twice !\n";
+	     flush stderr
+	   end
+       with Not_found -> () end;
+       Hashtbl.add tab f d) 
+    l
+
+let usage () =
+  print_string 
+  "[ usage: coqdep [-w] [-I dir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
+  flush stdout;
+  exit 1
+
+let add_coqlib_known dir_name f =
+  let complete_name = Filename.concat dir_name f 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,Some dir_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 (Filename.concat d1 d2) 
+    in
+    let complete_name = file_name (name,dirname) in
+    match try (stat (file_name (name,dirname))).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 -> Filename.concat 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 (basename,dirname)
+      | _ -> ()
+    in 
+    let add_known dir_name f =
+      let complete_name = Filename.concat dir_name 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 dir_name)
+	    else if Filename.check_suffix f ".ml4" then
+	      let basename = Filename.chop_suffix f ".ml4" in
+	      addQueue mlKnown (basename,Some dir_name)
+	    else if Filename.check_suffix f ".mli" then
+	      let basename = Filename.chop_suffix f ".mli" in
+	      addQueue mliKnown (basename,Some dir_name)
+	    else if Filename.check_suffix f ".v" then
+	      let basename = Filename.chop_suffix f ".v" in
+	      addQueue vKnown (basename,Some dir_name)
+        | _ -> ()
+    in
+    let add_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_known dir_name (readdir dir) done
+	     with End_of_file -> closedir dir)
+        | _ -> ()
+    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
+      | "-I" :: (r :: ll) -> add_directory r; parse ll
+      | "-I" :: [] -> 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
+    parse (List.tl (Array.to_list Sys.argv));
+    let theories = Filename.concat !coqlib "theories" in
+    List.iter
+      (fun s -> add_coqlib_directory (Filename.concat theories s))
+      Coq_config.theories_dirs;
+    let tactics = Filename.concat !coqlib "tactics" in
+    add_coqlib_directory tactics;
+    List.iter 
+      (fun s -> add_coqlib_directory (Filename.concat tactics s))
+      Coq_config.tactics_dirs;
+    mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu);
+    mlKnown  := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu);
+    vKnown   := !vKnown @ !vAccu;
+    warning_mult ".mli" !mliKnown;
+    warning_mult ".ml" !mlKnown;
+    warning_mult ".v" !vKnown;
+    if !option_c & not !option_D then mL_dependencies ();
+    if not !option_D then coq_dependencies ();
+    if !option_w or !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 000000000..d12e8518f
--- /dev/null
+++ b/tools/coqdep_lexer.mll
@@ -0,0 +1,199 @@
+{
+ 
+  (* $Id: *)
+  
+  open Lexing
+   
+  type mL_token = Use_module of string
+
+  type spec = bool
+		
+  type coq_token = 
+    | Require of spec * string
+    | RequireString of spec * string
+    | Declare of string list
+
+  let mlAccu  = ref ([] : (string * string * string option) list) 
+  and mliAccu = ref ([] : (string * string * string option) list) 
+  and vAccu   = ref ([] : (string * string option) list)
+
+  let mlKnown     = ref ([] : (string * string option) list) 
+  and mliKnown    = ref ([] : (string * string option) list) 
+  and vKnown      = ref ([] : (string * string option) list) 
+  and coqlibKnown = ref ([] : (string * string option) list)
+
+  let coqlib = ref Coq_config.coqlib
+		 
+  let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151
+						     
+  let addQueue q v = q := v :: !q
+		       
+  let file_name = function
+    | (s,None)     -> s 
+    | (s,Some ".") -> s
+    | (s,Some d)   -> Filename.concat d s
+
+  let comment_depth = ref 0
+ 
+  exception Fin_fichier
+    
+  let module_name = ref ""
+		      
+  let specif = ref false
+		 
+  let mllist = ref ([] : string list)
+}
+
+let space = [' ' '\t' '\n']
+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']+
+
+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}
+  | "\""
+      { 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*
+      { 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 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_end lexbuf }
+
+and opened_file_end = parse
+  | '.'               { Require (!specif, !module_name) }
+  | space+            { opened_file_end lexbuf }
+  | "(*"              { comment_depth := 1; comment lexbuf;
+      	       	       	opened_file_end lexbuf }
+  | '"' [^'"']* '"'   { let lex = Lexing.lexeme lexbuf in
+      	       	       	let str = String.sub lex 1 (String.length lex - 2) in
+			RequireString (!specif, str) }
+  | eof		      { raise Fin_fichier }
+  | _		      { opened_file_end 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 !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/gallina.1 b/tools/gallina.1
new file mode 100755
index 000000000..8c607216e
--- /dev/null
+++ b/tools/gallina.1
@@ -0,0 +1,74 @@
+.TH COQ 1 "29 March 1995" "Coq tools"
+
+.SH NAME
+gallina \- extracts specification from Coq vernacular files
+
+.SH SYNOPSIS
+.B gallina
+[
+.BI \-
+]
+[
+.BI \-stdout
+]
+[
+.BI \-nocomments
+]
+.I file ...
+
+.SH DESCRIPTION
+
+.B gallina 
+takes Coq files as arguments and builds the corresponding
+specification files.
+The Coq file
+.IR foo.v \&
+gives bearth to the specification file
+.IR foo.g. \&
+The suffix '.g' stands for Gallina.
+
+For that purpose, gallina removes all commands that follow a
+"Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it
+reaches a command "Abort.", "Save.", "Qed.", "Defined." or "Proof
+<...>.". It also removes every "Hint", "Syntax",
+"Immediate"  or "Transparent" command.
+
+Files without the .v suffix are ignored.
+
+
+.SH OPTIONS
+
+.TP
+.BI \-stdout
+Prints the result on standard output.
+.TP
+.BI \-
+Coq source is taken on standard input. The result is printed on
+standard output.
+.TP
+.BI \-nocomments
+Comments are removed in the *.g file.
+
+.SH NOTES
+
+Nested comments are correctly handled. In particular, every command
+"Save." or "Abort." in a comment is not taken into account.
+
+
+.SH BUGS
+
+Please report any bug to
+.B coq@pauillac.inria.fr
+
+
+
+
+
+
+	
+
+	
+
+	
+
+	
diff --git a/tools/gallina.ml b/tools/gallina.ml
new file mode 100644
index 000000000..f013c5788
--- /dev/null
+++ b/tools/gallina.ml
@@ -0,0 +1,59 @@
+
+(* $Id$ *)
+
+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 000000000..4a7568a18
--- /dev/null
+++ b/tools/gallina_lexer.mll
@@ -0,0 +1,118 @@
+
+(* $Id$ *)
+
+{
+ 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']
+
+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 }
+  | "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
+  | '.'   { 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
+  | '.'   { 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
+  | '.'   { 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 }