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

9 files changed, 487 insertions, 216 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 3339b1db..5bcbed64 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -10,7 +10,7 @@
 
 (*s Output options *)
 
-type target_language = LaTeX | HTML | TeXmacs
+type target_language = LaTeX | HTML | TeXmacs | Raw
 
 let target_language = ref HTML
 
@@ -57,6 +57,7 @@ let externals = ref true
 let coqlib = ref "http://coq.inria.fr/library/"
 let coqlib_path = ref Coq_config.coqlib
 let raw_comments = ref false
+let interpolate = ref false
 
 let charset = ref "iso-8859-1"
 let inputenc = ref ""
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 65c39b7a..a9a99706 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -25,7 +25,7 @@ body { padding: 0px 0px;
        padding: 10px;
        overflow: hidden;
        font-size: 100%;
-       line-height: 80% }
+       line-height: 100% }
 
 #main  a.idref:visited {color : #416DFF; text-decoration : none; }
 #main  a.idref:link {color : #416DFF; text-decoration : none; }
@@ -43,8 +43,6 @@ body { padding: 0px 0px;
 #main .section { background-color:#90bdff;
                  font-size : 175% }
 
-#main code { font-family: monospace }
-
 #main .doc { margin: 0px;
              padding: 10px;
              font-family: sans-serif;
@@ -55,7 +53,13 @@ body { padding: 0px 0px;
              background-color: #90bdff;
              border-style: plain}
 
-#main .doc code { font-family: monospace} 
+.inlinecode { 
+    display: inline;
+    font-family: monospace } 
+
+.code { 
+    display: block;
+    font-family: monospace } 
 
 /* Pied de page */
 
@@ -66,3 +70,29 @@ body { padding: 0px 0px;
 #footer a:link { text-decoration: none; 
                  color: #888888; }
 
+.id { display: inline; }
+
+.id[type="constructor"] { 
+    color: rgb(60%,0%,0%);
+}
+
+.id[type="var"] { 
+    color: rgb(40%,0%,40%);
+}
+
+.id[type="definition"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="lemma"] { 
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="inductive"] { 
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="keyword"] { 
+ color : #cf1d1d;
+/*     color: black; */
+}
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index d31314c5..ef4f4119 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -27,6 +27,11 @@
 %HEVEA\renewcommand{\medskip}{}
 %HEVEA\renewcommand{\bigskip}{}
 
+
+%HEVEA\newcommand{\lnot}{\coqwkw{not}}
+%HEVEA\newcommand{\lor}{\coqwkw{or}}
+%HEVEA\newcommand{\land}{\&}
+
 % own name
 \newcommand{\coqdoc}{\textsf{coqdoc}}
 
@@ -39,7 +44,7 @@
 \newcommand{\coqdockw}[1]{\texttt{#1}}
 
 % macro for typesetting variable identifiers
-\newcommand{\coqdocid}[1]{\textit{#1}}
+\newcommand{\coqdocvar}[1]{\textit{#1}}
 
 % macro for typesetting constant identifiers
 \newcommand{\coqdoccst}[1]{\textsf{#1}}
@@ -57,52 +62,93 @@
 % macro for typesetting constructor identifiers
 \newcommand{\coqdocconstr}[1]{\textsf{#1}}
 
+% macro for typesetting tactic identifiers
+\newcommand{\coqdoctac}[1]{\texttt{#1}}
+
+
+% Environment encompassing code fragments
+% !!! CAUTION: This environment may have empty contents
+\newenvironment{coqdoccode}{}{}
+
 % newline and indentation 
 %BEGIN LATEX
-\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par}
-\newcommand{\coqdocindent}[1]{\noindent\kern#1}
-%END LATEX
-%HEVEA\newcommand{\coqdoceol}{\begin{rawhtml}<BR>\end{rawhtml}}
-%HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}}
+% Base indentation length
+\newlength{\coqdocbaseindent}
+\setlength{\coqdocbaseindent}{0em}
+
+% Beginning of a line without any Coq indentation
+\newcommand{\coqdocnoindent}{\noindent\kern\coqdocbaseindent}
+% Beginning of a line with a given Coq indentation
+\newcommand{\coqdocindent}[1]{\noindent\kern\coqdocbaseindent\noindent\kern#1}
+% End-of-the-line
+\newcommand{\coqdoceol}{\hspace*{\fill}\setlength\parskip{0pt}\par}
+% Empty lines (in code only)
+\newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em}
 
 % macro for typesetting the title of a module implementation
 \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
 }
 \usepackage{ifpdf}
 \ifpdf
-  \usepackage[pdftex]{hyperref}
+  \RequirePackage{hyperref}
   \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}
-  \usepackage[all]{hypcap}
+
+  % To do indexing, use something like:
+  % \usepackage{multind}
+  % \newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
 
   \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
   \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
   \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
   \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
-    \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}}
+    \hypertarget{coq:#1}{\chapter{Library \texorpdfstring{\coqdoccst}{}{#2}}}}
 \else
   \newcommand{\coqdef}[3]{#3}
   \newcommand{\coqref}[2]{#2}
-  \newcommand{\identref}[2]{\textsf {#2}}
+  \newcommand{\texorpdfstring}[2]{#1}
+  \newcommand{\identref}[2]{\textsf{#2}}
   \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
 \fi
 \usepackage{xr}
 
-%\usepackage{color}
-%\usepackage{multind}
-%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
-
-  
-
-\newcommand{\coqdocvar}[1]{{\textit{#1}}}
-\newcommand{\coqdoctac}[1]{{\texttt{#1}}}
-
+\newif\if@coqdoccolors
+  \@coqdoccolorsfalse
+
+\DeclareOption{color}{\@coqdoccolorstrue}
+\ProcessOptions
+
+\if@coqdoccolors
+\RequirePackage{xcolor}
+\definecolor{varpurple}{rgb}{0.4,0,0.4}
+\definecolor{constrmaroon}{rgb}{0.6,0,0}
+\definecolor{defgreen}{rgb}{0,0.4,0}
+\definecolor{indblue}{rgb}{0,0,0.8}
+\definecolor{kwred}{rgb}{0.8,0.1,0.1}
+
+\def\coqdocvarcolor{varpurple}
+\def\coqdockwcolor{kwred}
+\def\coqdoccstcolor{defgreen}
+\def\coqdocindcolor{indblue}
+\def\coqdocconstrcolor{constrmaroon}
+\def\coqdocmodcolor{defgreen}
+\def\coqdocaxcolor{varpurple}
+\def\coqdoctaccolor{black}
+
+\def\coqdockw#1{{\color{\coqdockwcolor}{\texttt{#1}}}}
+\def\coqdocvar#1{{\color{\coqdocvarcolor}{\textit{#1}}}}
+\def\coqdoccst#1{{\color{\coqdoccstcolor}{\textrm{#1}}}}
+\def\coqdocind#1{{\color{\coqdocindcolor}{\textsf{#1}}}}
+\def\coqdocconstr#1{{\color{\coqdocconstrcolor}{\textsf{#1}}}}
+\def\coqdocmod#1{{{\color{\coqdocmodcolor}{\textsc{\textsf{#1}}}}}}
+\def\coqdocax#1{{{\color{\coqdocaxcolor}{\textsl{\textrm{#1}}}}}}
+\def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}}
+\fi
 
 \newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
 \newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
 
-%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
-%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
-\newcommand{\coqvariable}[2]{\coqdocid{#2}}
+\newcommand{\coqvariable}[2]{\coqdocvar{#2}}
+\newcommand{\coqvariableref}[2]{\coqref{#1}{\coqdocvar{#2}}}
 
 \newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
 \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
@@ -133,8 +179,8 @@
 
 \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
 
-\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+\newcommand{\coqsection}[2]{\coqdef{sec:#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqsectionref}[2]{\coqref{sec:#1}{\coqdoccst{#2}}}
 
 %\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
   
@@ -145,11 +191,7 @@
 \newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
 \newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
 
-\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}}
-\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}}
-
-
-%HEVEA\newcommand{\lnot}{\coqwkw{not}}
-%HEVEA\newcommand{\lor}{\coqwkw{or}}
-%HEVEA\newcommand{\land}{\&}
+\newcommand{\coqmodule}[2]{\coqdef{mod:#1}{#2}{\coqdocmod{#2}}}
+\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}}
 
+\endinput
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 1da8ebd7..56a3cd11 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mli 11065 2008-06-06 22:39:43Z msozeau $ i*)
+(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 open Cdglobals
 
@@ -40,6 +40,8 @@ type index_entry =
 
 val find : coq_module -> loc -> index_entry
 
+val find_string : coq_module -> string -> index_entry
+
 val add_module : coq_module -> unit
 
 type module_kind = Local | Coqlib | Unknown
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index fc2090dc..f8adb52b 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mll 11065 2008-06-06 22:39:43Z msozeau $ i*)
+(*i $Id: index.mll 11790 2009-01-15 20:19:58Z msozeau $ i*)
 
 {
 
@@ -47,9 +47,14 @@ let current_type = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
-let table = Hashtbl.create 97
-  (** [table] is used to store references and definitions *)
+(** [deftable] stores only definitions and is used to interpolate idents 
+    inside comments, which are not globalized otherwise. *)
 
+let deftable = Hashtbl.create 97
+
+(** [reftable] stores references and definitions *)
+let reftable = Hashtbl.create 97
+  
 let full_ident sp id =
   if sp <> "<>" then 
     if id <> "<>" then 
@@ -60,15 +65,24 @@ let full_ident sp id =
   else ""
     
 let add_def loc ty sp id = 
-  Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
-
+  Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
+  Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+    
 let add_ref m loc m' sp id ty = 
-  Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty))
+  if Hashtbl.mem reftable (m, loc) then ()
+  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+  let idx = if id = "<>" then m' else id in
+    if Hashtbl.mem deftable idx then ()
+    else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))  
     
-let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
-
-let find m l = Hashtbl.find table (m, l)
-
+let add_mod m loc m' id = 
+  Hashtbl.add reftable (m, loc) (Mod (m', id));
+  Hashtbl.add deftable m (Mod (m', id))
+    
+let find m l = Hashtbl.find reftable (m, l)
+  
+let find_string m s = Hashtbl.find deftable s
+  
 (*s Manipulating path prefixes *) 
 
 type stack = string list 
@@ -216,7 +230,7 @@ let all_entries () =
     | Def (s,t) -> add_g s m t; add_bt t s m
     | Ref _ | Mod _ -> ()
   in
-    Hashtbl.iter classify table;
+    Hashtbl.iter classify reftable;
     Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
     { idx_name = "global"; 
       idx_entries = sort_entries !gl; 
@@ -238,7 +252,9 @@ let firstchar =
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
      '\'' '0'-'9']
-let ident = firstchar identchar*
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let ident = id | pfx_id id
 
 let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
 let end_hide = "(*" space* "end" space+ "hide" space* "*)"
@@ -406,9 +422,9 @@ and module_refs = parse
   | ident  
       { let id =  lexeme lexbuf in
 	  (try
-	      add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
-	    with
-		Not_found -> ()
+	     add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
+	   with
+	       Not_found -> ()
 	  ); 
 	module_refs lexbuf }
   | eof    
@@ -418,7 +434,7 @@ and module_refs = parse
 
 {
   let type_of_string = function
-    | "def" | "coe" | "subclass" | "canonstruc" 
+    | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
     | "ex" | "scheme" -> Definition
     | "prf" | "thm" -> Lemma
     | "ind" | "coind" -> Inductive
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 81560259..2e97618b 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 11236 2008-07-18 15:58:12Z notin $ i*)
+(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -30,6 +30,7 @@ let usage () =
   prerr_endline "  --html               produce a HTML document (default)";
   prerr_endline "  --latex              produce a LaTeX document";
   prerr_endline "  --texmacs            produce a TeXmacs document";
+  prerr_endline "  --raw                produce a text document";
   prerr_endline "  --dvi                output the DVI";
   prerr_endline "  --ps                 output the PostScript";
   prerr_endline "  --pdf                output the Pdf";
@@ -56,12 +57,14 @@ let usage () =
   prerr_endline "  --no-externals       no links to Coq standard library";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
   prerr_endline "                       (default is http://coq.inria.fr/library/)";
+  prerr_endline "  --boot               run in boot mode";
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  --latin1             set ISO-8859-1 input language";
   prerr_endline "  --utf8               set UTF-8 input language";
   prerr_endline "  --charset <string>   set HTML charset";
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
+  prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
   prerr_endline "";
   exit 1
 
@@ -81,6 +84,7 @@ let banner () =
 let target_full_name f = 
   match !Cdglobals.target_language with
     | HTML -> f ^ ".html"
+    | Raw -> f ^ ".txt"
     | _ -> f ^ ".tex"
 	
 (*s \textbf{Separation of files.} Files given on the command line are
@@ -257,6 +261,8 @@ let parse () =
 	Cdglobals.target_language := HTML; parse_rec rem
     | ("-texmacs" | "--texmacs") :: rem ->
 	Cdglobals.target_language := TeXmacs; parse_rec rem
+    | ("-raw" | "--raw") :: rem ->
+	Cdglobals.target_language := Raw; parse_rec rem
     | ("-charset" | "--charset") :: s :: rem ->
 	Cdglobals.charset := s; parse_rec rem
     | ("-charset" | "--charset") :: [] ->
@@ -267,6 +273,9 @@ let parse () =
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
 	Cdglobals.raw_comments := true; parse_rec rem
+    | ("-interpolate" | "--interpolate") :: rem ->
+	Cdglobals.interpolate := true; parse_rec rem
+
     | ("-latin1" | "--latin1") :: rem ->
 	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
@@ -310,6 +319,8 @@ let parse () =
 	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
+    | ("--boot" | "-boot") :: rem ->
+	Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
@@ -318,6 +329,7 @@ let parse () =
 	add_file (what_file f); parse_rec rem
   in 
     parse_rec (List.tl (Array.to_list Sys.argv));
+    Output.initialize ();
     List.rev !files
 
       
@@ -414,10 +426,10 @@ let read_glob x =
   match x with
     | Vernac_file (f,m) ->   
 	let glob = (Filename.chop_extension f) ^ ".glob" in
-	  (try
+ 	  (try
 	      Vernac_file (f, Index.read_glob glob)
-	    with _ -> 
-	      eprintf "Warning: file %s cannot be opened; links will not be available\n" glob;
+            with e -> 
+              eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
 	      x)
   | Latex_file _ -> x
 
@@ -430,13 +442,13 @@ let produce_document l =
   (if !target_language=HTML then
     let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
     let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
-      copy src dst);
+      if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
   (if !target_language=LaTeX then
       let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
       let dst = if !output_dir <> "" then 
 	  Filename.concat !output_dir "coqdoc.sty" 
 	else "coqdoc.sty" in
-	copy src dst);
+	if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
   (match !Cdglobals.glob_source with
     | NoGlob -> ()
     | DotGlob -> ignore (List.map read_glob l)
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 93414f22..c146150c 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 11154 2008-06-19 18:42:19Z msozeau $ i*)
+(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -32,43 +32,48 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint";
-      "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
+    [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+      "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
       "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
       "Module"; "Module Type"; "Declare Module"; "Include";
-      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
+      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-      "Set"; "Unset"; "Variable"; "Variables"; "Context";
+      "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; 
       "Boxed"; "Unboxed"; "Inline";
-      "Arguments"; "Add"; "Strict";
-      "Typeclasses"; "Instance"; "Class"; "Instantiation";
+      "Implicit Arguments"; "Add"; "Strict";
+      "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
+      "subgoal";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
-      "Program Instance";
+      "Program Instance"; "Equations"; "Equations_nocomp";
       (*i (* coq terms *) *)
-	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
-	"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
+      "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
+      "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      (* Ltac *)
+      "before"; "after"
        ]
 
 let is_tactic = 
   build_table
-    [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
-      "destruct"; "induction"; "elim"; "dependent"; 
-      "generalize"; "clear"; "rename"; "move"; "set"; "assert";
-      "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
+    [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
+      "elimtype"; "progress"; "setoid_rewrite";
+      "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
+      "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
+      "set"; "assert"; "do"; "repeat";
+      "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate";
       "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
-      "pattern"; "intuition"; "congruence";
+      "pattern"; "intuition"; "congruence"; "fail"; "fresh";
       "trivial"; "exact"; "tauto"; "firstorder"; "ring";
-      "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
+      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
 
 (*s Current Coq module *)
 
@@ -92,27 +97,31 @@ let find_printing_token tok =
 let remove_printing_token = Hashtbl.remove token_pp
 
 (* predefined pretty-prints *)
-let _ = List.iter 
-	  (fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
-	  [ "*" ,  "\\ensuremath{\\times}";
-	    "|", "\\ensuremath{|}";
-	    "->",  "\\ensuremath{\\rightarrow}";
-	    "->~",  "\\ensuremath{\\rightarrow\\lnot}";
-	    "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}";
-	    "<-",  "\\ensuremath{\\leftarrow}";
-	    "<->", "\\ensuremath{\\leftrightarrow}";
-	    "=>",  "\\ensuremath{\\Rightarrow}";
-	    "<=",  "\\ensuremath{\\le}";
-	    ">=",  "\\ensuremath{\\ge}";
-	    "<>",  "\\ensuremath{\\not=}";
-	    "~",   "\\ensuremath{\\lnot}";
-	    "/\\", "\\ensuremath{\\land}";
-	    "\\/", "\\ensuremath{\\lor}";
-	    "|-",  "\\ensuremath{\\vdash}";
-	    "forall", "\\ensuremath{\\forall}";
-	    "exists", "\\ensuremath{\\exists}";
-	    (* "fun", "\\ensuremath{\\lambda}" ? *)
-	  ]
+let initialize () = 
+  let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
+    List.iter 
+      (fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l'))
+      [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
+	"|", "\\ensuremath{|}", None;
+	"->",  "\\ensuremath{\\rightarrow}", if_utf8 "→";
+	"->~",  "\\ensuremath{\\rightarrow\\lnot}", None;
+	"->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}", None;
+	"<-",  "\\ensuremath{\\leftarrow}", None;
+	"<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔";
+	"=>",  "\\ensuremath{\\Rightarrow}", if_utf8 "⇒";
+	"<=",  "\\ensuremath{\\le}", if_utf8 "≤";
+	">=",  "\\ensuremath{\\ge}", if_utf8 "≥";
+	"<>",  "\\ensuremath{\\not=}", if_utf8 "≠";
+	"~",   "\\ensuremath{\\lnot}", if_utf8 "¬";
+	"/\\", "\\ensuremath{\\land}", if_utf8 "∧";
+	"\\/", "\\ensuremath{\\lor}", if_utf8 "∨";
+	"|-",  "\\ensuremath{\\vdash}", None;
+	"forall", "\\ensuremath{\\forall}", if_utf8 "∀";
+	"exists", "\\ensuremath{\\exists}", if_utf8 "∃";
+	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
+	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ"
+	(* "fun", "\\ensuremath{\\lambda}" ? *)
+      ]
 
 (*s Table of contents *)
 
@@ -130,6 +139,9 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r
 
 module Latex = struct
 
+  let in_title = ref false
+  let in_doc = ref false
+
   (*s Latex preamble *)
 
   let (preamble : string Queue.t) = Queue.create ()
@@ -208,7 +220,7 @@ module Latex = struct
 
   let indentation n = 
     if n == 0 then 
-      printf "\\noindent\n"
+      printf "\\coqdocnoindent\n"
     else
       let space = 0.5 *. (float n) in
       printf "\\coqdocindent{%2.2fem}\n" space
@@ -243,35 +255,49 @@ module Latex = struct
 	  let _m = Filename.concat !coqlib m in
 	    printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
       | Coqlib | Unknown ->
-	  raw_ident s
+	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
 
   let defref m id ty s =
     printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
 
+  let reference s = function
+    | Def (fullid,typ) -> 
+	defref !current_module fullid typ s
+    | Mod (m,s') when s = s' ->
+	module_ref m s
+    | Ref (m,fullid,typ) -> 
+	ident_ref m fullid typ s
+    | Mod _ ->
+	printf "\\coqdocvar{"; raw_ident s; printf "}"
+	  
   let ident s loc = 
     if is_keyword s then begin
       printf "\\coqdockw{"; raw_ident s; printf "}"
     end else begin
       begin
 	try
-	  (match Index.find !current_module loc with
-	     | Def (fullid,typ) -> 
-		 defref !current_module fullid typ s
-             | Mod (m,s') when s = s' ->
-		 module_ref m s
-	     | Ref (m,fullid,typ) -> 
-		 ident_ref m fullid typ s
-	     | Mod _ ->
-		 printf "\\coqdocid{"; raw_ident s; printf "}")
+	  reference s (Index.find !current_module loc)
 	with Not_found ->
 	  if is_tactic s then begin
 	    printf "\\coqdoctac{"; raw_ident s; printf "}"
-	  end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end
+	  end else begin
+	    if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) 
+	    then
+	      try reference s (Index.find_string !current_module s)
+	      with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
+	    else (printf "\\coqdocvar{"; raw_ident s; printf "}")
+	  end
       end
     end
 
-  let ident s l = with_latex_printing (fun s -> ident s l) s
-
+  let ident s l = 
+    if !in_title then (
+      printf "\\texorpdfstring{";
+      with_latex_printing (fun s -> ident s l) s;
+      printf "}{"; raw_ident s; printf "}")
+    else
+      with_latex_printing (fun s -> ident s l) s
+    
   let symbol = with_latex_printing raw_ident
 
   let rec reach_item_level n = 
@@ -290,13 +316,13 @@ module Latex = struct
 
   let stop_item () = reach_item_level 0
 
-  let start_doc () = printf "\n\n\n\\noindent\n"
+  let start_doc () = in_doc := true
 
-  let end_doc () = stop_item (); printf "\n\n\n"
+  let end_doc () = in_doc := false; stop_item ()
 
-  let start_coq () = ()
+  let start_coq () = printf "\\begin{coqdoccode}\n"
 
-  let end_coq () = ()
+  let end_coq () = printf "\\end{coqdoccode}\n"
 
   let start_code () = end_doc (); start_coq ()
 
@@ -312,17 +338,17 @@ module Latex = struct
   let section lev f =
     stop_item ();
     output_string (section_kind lev);
-    f ();
+    in_title := true; f (); in_title := false;
     printf "}\n\n"
 
   let rule () =
     printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}"
 
-  let paragraph () = stop_item (); printf "\n\n\\medskip\n"
+  let paragraph () = stop_item (); printf "\n\n"
 
   let line_break () = printf "\\coqdoceol\n"
 
-  let empty_line_of_code () = printf "\n\n\\medskip\n"
+  let empty_line_of_code () = printf "\\coqdocemptyline\n"
 
   let start_inline_coq () = ()
 
@@ -394,7 +420,8 @@ module Html = struct
 
   let line_break () = printf "<br/>\n"
 
-  let empty_line_of_code () = printf "\n<br/>\n"
+  let empty_line_of_code () = 
+    printf "\n<br/>\n"
 
   let char = function
     | '<' -> printf "&lt;"
@@ -417,49 +444,54 @@ module Html = struct
   let stop_verbatim () = printf "</pre>\n"
 
   let module_ref m s = 
-    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    (*i
-    match find_module m with
-    | Local ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib when !externals ->
-	let m = Filename.concat !coqlib m in
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib | Unknown ->
-	raw_ident s
-    i*)
-
-  let ident_ref m fid s = 
     match find_module m with
       | Local ->
-	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+	  printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
       | Coqlib when !externals ->
 	  let m = Filename.concat !coqlib m in
-	    printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+	    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
       | Coqlib | Unknown ->
 	  raw_ident s
 
+  let ident_ref m fid typ s =
+    match find_module m with
+    | Local ->
+	printf "<span class=\"id\" type=\"%s\">" typ; 
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
+	printf "</a></span>"
+    | Coqlib when !externals ->
+	let m = Filename.concat !coqlib m in
+	  printf "<span class=\"id\" type=\"%s\">" typ; 
+	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
+	  raw_ident s; printf "</a></span>"
+    | Coqlib | Unknown ->
+	printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
+	  
   let ident s loc = 
     if is_keyword s then begin
-      printf "<span class=\"keyword\">"; 
+      printf "<span class=\"id\" type=\"keyword\">"; 
       raw_ident s; 
       printf "</span>"
     end else 
       begin
 	try
 	  (match Index.find !current_module loc with
-	     | Def (fullid,_) -> 
-		 printf "<a name=\"%s\"></a>" fullid; raw_ident s
+	     | Def (fullid,ty) -> 
+		 printf "<span class=\"id\" type=\"%s\">" (type_name ty); 
+		 printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
              | Mod (m,s') when s = s' ->
 		 module_ref m s
 	     | Ref (m,fullid,ty) -> 
-		 ident_ref m fullid s
+		 ident_ref m fullid (type_name ty) s
 	     | Mod _ ->
-		 raw_ident s)
+		 printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>")
 	with Not_found ->
-	  raw_ident s
+	  if is_tactic s then
+	    (printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
+	  else
+	    (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
       end
-	  
+
   let with_html_printing f tok =
     try 
       (match Hashtbl.find token_pp tok with
@@ -488,9 +520,9 @@ module Html = struct
 
   let stop_item () = reach_item_level 0
 
-  let start_coq () = if not !raw_comments then printf "<code>\n"
+  let start_coq () = if not !raw_comments then printf "<div class=\"code\">\n"
 
-  let end_coq () = if not !raw_comments then printf "</code>\n"
+  let end_coq () = if not !raw_comments then printf "</div>\n"
 
   let start_doc () = 
     if not !raw_comments then
@@ -504,9 +536,9 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = printf "<code>"
+  let start_inline_coq () = printf "<span class=\"inlinecode\">"
 
-  let end_inline_coq () = printf "</code>"
+  let end_inline_coq () = printf "</span>"
 
   let paragraph () = stop_item (); printf "\n<br/><br/>\n"
 
@@ -539,7 +571,7 @@ module Html = struct
   let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
 
   (* Construction d'une liste des index (1 index global, puis 1
-     index par catégorie) *)
+     index par catégorie) *)
   let format_global_index =
     Index.map 
       (fun s (m,t) -> 
@@ -578,7 +610,7 @@ module Html = struct
     printf "</table>\n"
 	
   let make_one_multi_index prt_tbl i =
-    (* Attn: make_one_multi_index créé un nouveau fichier... *)
+    (* Attn: make_one_multi_index créé un nouveau fichier... *)
     let idx = i.idx_name in
     let one_letter ((c,l) as cl) =
       open_out_file (sprintf "index_%s_%c.html" idx c);
@@ -776,68 +808,155 @@ module TeXmacs = struct
 
 end
 
+
+(*s LaTeX output *)
+
+module Raw = struct
+
+  let header () = ()
+
+  let trailer () = ()
+
+  let char = output_char
+
+  let label_char c = match c with
+    | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
+    | '^' | '~' -> ()
+    | _ -> 
+	output_char c
+
+  let latex_char = output_char
+  let latex_string = output_string
+
+  let html_char _ = ()
+  let html_string _ = ()
+
+  let raw_ident s =
+    for i = 0 to String.length s - 1 do char s.[i] done
+
+  let start_module () = ()
+  let end_module () = ()
+
+  let start_latex_math () = ()
+  let stop_latex_math () = ()
+
+  let start_verbatim () = ()
+
+  let stop_verbatim () = ()
+
+  let indentation n = 
+      for i = 1 to n do printf " " done
+
+  let ident s loc = raw_ident s
+
+  let symbol = raw_ident
+
+  let item n = printf "- "
+
+  let stop_item () = ()
+
+  let start_doc () = printf "(** "
+  let end_doc () = printf " *)\n"
+
+  let start_coq () = ()
+  let end_coq () = ()
+
+  let start_code () = end_doc (); start_coq ()
+  let end_code () = end_coq (); start_doc ()
+
+  let section_kind = 
+    function
+      | 1 -> "*"
+      | 2 -> "**"
+      | 3 -> "***"
+      | 4 -> "****"
+      | _ -> assert false    
+
+  let section lev f = 
+    output_string (section_kind lev);
+    f ()
+
+  let rule () = ()
+
+  let paragraph () = printf "\n\n"
+
+  let line_break () = printf "\n"
+
+  let empty_line_of_code () = printf "\n"
+
+  let start_inline_coq () = ()
+  let end_inline_coq () = ()
+
+  let make_multi_index () = ()
+  let make_index () = ()
+  let make_toc () = () 
+
+end
+
+
+
 (*s Generic output *)
 
-let select f1 f2 f3 x = 
-  match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x
+let select f1 f2 f3 f4 x = 
+  match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x
 
 let push_in_preamble = Latex.push_in_preamble
 
-let header = select Latex.header Html.header TeXmacs.header
-let trailer = select Latex.trailer Html.trailer TeXmacs.trailer
+let header = select Latex.header Html.header TeXmacs.header Raw.header
+let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer
 
 let start_module = 
-  select Latex.start_module Html.start_module TeXmacs.start_module
+  select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module
 
-let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc
-let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc
+let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
+let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc
 
-let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq
-let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq
+let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
+let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
 
-let start_code = select Latex.start_code Html.start_code TeXmacs.start_code
-let end_code = select Latex.end_code Html.end_code TeXmacs.end_code
+let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code
+let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code 
 
 let start_inline_coq = 
-  select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq
+  select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq
 let end_inline_coq = 
-  select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq
+  select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq
 
-let indentation = select Latex.indentation Html.indentation TeXmacs.indentation
-let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph
-let line_break = select Latex.line_break Html.line_break TeXmacs.line_break
+let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation
+let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph
+let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break
 let empty_line_of_code = select 
-  Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code
+  Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code
 
-let section = select Latex.section Html.section TeXmacs.section
-let item = select Latex.item Html.item TeXmacs.item
-let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item
-let rule = select Latex.rule Html.rule TeXmacs.rule
+let section = select Latex.section Html.section TeXmacs.section Raw.section
+let item = select Latex.item Html.item TeXmacs.item Raw.item
+let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item
+let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
-let char = select Latex.char Html.char TeXmacs.char
-let ident = select Latex.ident Html.ident TeXmacs.ident
-let symbol = select Latex.symbol Html.symbol TeXmacs.symbol
+let char = select Latex.char Html.char TeXmacs.char Raw.char
+let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
+let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol
 
-let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char
+let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char
 let latex_string = 
-  select Latex.latex_string Html.latex_string TeXmacs.latex_string
-let html_char = select Latex.html_char Html.html_char TeXmacs.html_char
+  select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string
+let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char
 let html_string = 
-  select Latex.html_string Html.html_string TeXmacs.html_string
+  select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string
 
 let start_latex_math = 
-  select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math
+  select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
 let stop_latex_math = 
-  select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math
+  select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math
 
 let start_verbatim = 
-  select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim
+  select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
 let stop_verbatim = 
-  select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim
+  select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
 let verbatim_char = 
-  select output_char Html.char TeXmacs.char
+  select output_char Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
-let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index
-let make_index = select Latex.make_index Html.make_index TeXmacs.make_index
-let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc
+let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index
+let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index
+let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 87b311f3..3da80335 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 8669 2006-03-28 17:34:15Z notin $ i*)
+(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 open Cdglobals
 open Index
 
+val initialize : unit -> unit
+
 val add_printing_token : string -> string option * string option -> unit
 val remove_printing_token : string -> unit
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index baace5ba..3ae5cbed 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 11255 2008-07-24 16:57:13Z notin $ i*)
+(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -57,6 +57,7 @@
   let formatted = ref false
   let brackets = ref 0
   let comment_level = ref 0
+  let in_proof = ref false
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
@@ -173,11 +174,12 @@ let firstchar =
   ['A'-'Z' 'a'-'z' '_' 
   (* iso 8859-1 accents *) 
   '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  (* *)
   '\194' '\185' |
   (* utf-8 latin 1 supplement *) 
   '\195' ['\128'-'\191'] |
   (* utf-8 letterlike symbols *) 
-  '\206' ['\177'-'\183'] |
+  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
@@ -188,17 +190,24 @@ let pfx_id = (id '.')*
 let identifier = 
   id | pfx_id id
 
-let symbolchar_no_brackets =
-  ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'
-   '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~'
-   '{' '}' '(' ')'] |
+let symbolchar_symbol_no_brackets =
+  ['!' '$' '%' '&' '*' '+' ',' '^' '#'
+      '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
   (* utf-8 symbols *) 
   '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
+let symbolchar_no_brackets = symbolchar_symbol_no_brackets | 
+    [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
 let symbolchar = symbolchar_no_brackets | '[' | ']'
-let token_no_brackets = symbolchar_no_brackets+
-let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
+let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
+let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
 let printing_token = (token | id)+
 
+(* tokens with balanced brackets *)
+let token_brackets =
+  ( token_no_brackets ('[' token_no_brackets? ']')* 
+  | token_no_brackets? ('[' token_no_brackets? ']')+ )
+  token_no_brackets?
+
 let thm_token = 
   "Theorem" 
   | "Lemma" 
@@ -208,22 +217,26 @@ let thm_token =
   | "Proposition" 
   | "Property"
   | "Goal"
+  | "Next" space+ "Obligation"
 
 let def_token = 
   "Definition" 
   | "Let" 
   | "Class"
-  | "SubClass" 
+  | "SubClass"
   | "Example"
   | "Local" 
   | "Fixpoint" 
+  | "Boxed" 
   | "CoFixpoint" 
   | "Record" 
   | "Structure" 
-  | "Instance"
   | "Scheme"
   | "Inductive"
   | "CoInductive"
+  | "Equations"
+  | "Instance"
+  | "Global" space+ "Instance"
 
 let decl_token = 
   "Hypothesis" 
@@ -277,6 +290,8 @@ let commands =
   | ("Hypothesis" | "Hypotheses")
   | "End"
 
+let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+
 let extraction = 
   "Extraction"
   | "Recursive" space+ "Extraction" 
@@ -291,7 +306,8 @@ let prog_kw =
   | "Solve"
 
 let gallina_kw_to_hide =
-  "Implicit"
+    "Implicit" space+ "Arguments"
+  | "Next" "Obligation"
   | "Ltac"
   | "Require"
   | "Import"
@@ -308,12 +324,6 @@ let gallina_kw_to_hide =
   | "Declare" space+ ("Left" | "Right") space+ "Step" 
 
 
-(* tokens with balanced brackets *)
-let token_brackets =
-  ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* 
-  | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ )
-  symbolchar_no_brackets*
-
 let section = "*" | "**" | "***" | "****"
 
 let item_space = "    "
@@ -333,7 +343,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { Output.empty_line_of_code (); coq_bol lexbuf }
+      { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -352,7 +362,7 @@ rule coq_bol = parse
       { let s = lexeme lexbuf in
 	  if !Cdglobals.light && section_or_end s then 
 	    let eol = skip_to_dot lexbuf in
-	      if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf
+	      if eol then (coq_bol lexbuf) else coq lexbuf
 	  else 
 	    begin
 	      let nbsp,isp = count_spaces s in
@@ -362,16 +372,45 @@ rule coq_bol = parse
 		  let eol = body lexbuf in 
 		    if eol then coq_bol lexbuf else coq lexbuf
 	    end }
-  | space* gallina_kw
+  | space* thm_token
       { let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	let s = String.sub s isp (String.length s - isp)  in
 	  Output.indentation nbsp;
 	  Output.ident s (lexeme_start lexbuf + isp); 
+	  let eol = body lexbuf in
+	    in_proof := true;
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space* "Proof" (space* "." | space+ "with")
+      { in_proof := true;
+	let eol = 
+	if not !Cdglobals.gallina then 
+	  begin backtrack lexbuf; body_bol lexbuf end 
+	else true
+	in if eol then coq_bol lexbuf else coq lexbuf }
+  | space* end_kw { 
+      let eol = 
+	if not (!in_proof && !Cdglobals.gallina) then 
+	  begin backtrack lexbuf; body_bol lexbuf end 
+	else
+	  skip_to_dot lexbuf 
+      in
+	in_proof := false;
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | space* gallina_kw
+      { 
+	in_proof := false;
+	let s = lexeme lexbuf in 
+	let nbsp,isp = count_spaces s in
+	let s = String.sub s isp (String.length s - isp)  in
+	  Output.indentation nbsp;
+	  Output.ident s (lexeme_start lexbuf + isp); 
 	  let eol= body lexbuf in
 	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* prog_kw
-      { let s = lexeme lexbuf in 
+      { 
+	in_proof := false;
+	let s = lexeme lexbuf in 
 	let nbsp,isp = count_spaces s in
 	  Output.indentation nbsp;
 	  let s = String.sub s isp (String.length s - isp)  in
@@ -409,7 +448,7 @@ rule coq_bol = parse
   | _
       { let eol = 
 	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end 
+	    begin backtrack lexbuf; body_bol lexbuf end 
 	  else 
 	    skip_to_dot lexbuf 
 	in
@@ -419,7 +458,7 @@ rule coq_bol = parse
 
 and coq = parse
   | nl 
-      { Output.line_break(); coq_bol lexbuf }
+      { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
@@ -448,6 +487,15 @@ and coq = parse
 	      let eol=body lexbuf in 
 		if eol then coq_bol lexbuf else coq lexbuf
 	    end }
+  | end_kw { 
+      let eol = 
+	if not (!in_proof && !Cdglobals.gallina) then 
+	  begin backtrack lexbuf; body lexbuf end 
+	else
+	  skip_to_dot lexbuf 
+      in
+	in_proof := false;
+	if eol then coq_bol lexbuf else coq lexbuf }
   | gallina_kw
       { let s = lexeme lexbuf in 
 	  Output.ident s (lexeme_start lexbuf); 
@@ -463,7 +511,7 @@ and coq = parse
       { () }
   | _ {	let eol = 
 	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; Output.indentation 0; body lexbuf end 
+	    begin backtrack lexbuf; body lexbuf end 
 	  else 
 	    let eol = skip_to_dot lexbuf in
 	      if eol then Output.line_break (); eol
@@ -496,16 +544,15 @@ and doc_bol = parse
 and doc = parse
   | nl
       { Output.char '\n'; doc_bol lexbuf }
-  | "["
-      { brackets := 1; 
-	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
-	doc lexbuf }
-  | "[[" nl space*
+  | "[[" nl
       { formatted := true; Output.line_break (); Output.start_inline_coq ();
-	Output.indentation (fst (count_spaces (lexeme lexbuf))); 
 	let eol = body_bol lexbuf in 
 	  Output.end_inline_coq (); formatted := false;
 	  if eol then doc_bol lexbuf else doc lexbuf}
+  | "["
+      { brackets := 1; 
+	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
+	doc lexbuf }
   | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
@@ -612,7 +659,7 @@ and skip_to_dot = parse
 and body_bol = parse
   | space+
       { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
-  | _ { backtrack lexbuf; body lexbuf }
+  | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
 
 and body = parse
   | nl {Output.line_break(); body_bol lexbuf}
@@ -645,7 +692,7 @@ and notation_bol = parse
 
 and notation = parse
   | nl { Output.line_break(); notation_bol lexbuf }
-  | '"' { Output.char '"'; false }
+  | '"' { Output.char '"'}
   | token
       { let s = lexeme lexbuf in
 	  Output.symbol s; notation lexbuf }
@@ -660,7 +707,7 @@ and skip_hide = parse
 (*s Reading token pretty-print *)
 
 and printing_token_body = parse
-  | "*)" | eof 
+  | "*)" nl? | eof 
 	{ let s = Buffer.contents token_buffer in 
 	  Buffer.clear token_buffer;
 	  s }