21 files changed, 82 insertions, 72 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore
index 90d61db14..4b0319acf 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -34,3 +34,4 @@ library.files.ls
 library.files.ls.tmp
 library.coqweb.tex
 tradv8
+coqide.eps
diff --git a/doc/Anomalies.tex b/doc/Anomalies.tex
index 8e23fa602..a21577db0 100755
--- a/doc/Anomalies.tex
+++ b/doc/Anomalies.tex
@@ -2,7 +2,7 @@
 
 \input{./title}
 
-\title{Known bugs of {\sf Coq} V6.2}
+\title{Known bugs of \Coq{} V6.2}
 \author{\ }
 \begin{document}
 \maketitle
diff --git a/doc/ChangesV7-0.tex b/doc/ChangesV7-0.tex
index 7b10f4f82..b593b9dc8 100755
--- a/doc/ChangesV7-0.tex
+++ b/doc/ChangesV7-0.tex
@@ -318,7 +318,7 @@ see the Library documentation for more information.
 
 \section{Tactics}
 \label{Tactics}
-\def\oc{{\sf Objective~Caml}}
+\def\oc{\textsc{Objective~Caml}}
 
 \subsection{A tactic language: $\ltac$}
 
@@ -334,7 +334,7 @@ $\ltac$ has been contributed by David Delahaye and, for more details, see the
 Reference Manual. Regarding the foundations of this language, the author page
 can be visited at the following URL:\\
 
-{\sf http://logical.inria.fr/\~{}delahaye/}
+\url{http://logical.inria.fr/~delahaye/}
 
 \paragraph{Tactic debugger}
 
@@ -345,7 +345,7 @@ can be visited at the following URL:\\
 
 \subsection{New tactics}
 \label{NewTactics}
-\def\ml{{\sf ML}}
+\def\ml{\textsc{ML}}
 
    \paragraph{{\tt Field}} written by David~Delahaye and Micaela~Mayero solves
 equalities using commutative field theory. This tactic is reflexive and has
diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 629b84530..2ef5c41c1 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -6,13 +6,12 @@
 \begin{flushleft}
   \em The status of extraction is experimental.
 \end{flushleft}
-We present here the \Coq\ extraction commands, used
-to build certified and relatively
-efficient functional programs, extracting them from the proofs of their
-specifications. 
-The functional languages available as output are currently 
-\ocaml\ and {\sf Haskell} and {\sf Scheme}. In the following, ``ML'' will be 
-used (abusively) to refer to any of the three.
+We present here the \Coq\ extraction commands, used to build certified
+and relatively efficient functional programs, extracting them from the
+proofs of their specifications.  The functional languages available as
+output are currently \ocaml{}, \textsc{Haskell} and \textsc{Scheme}.
+In the following, ``ML'' will be used (abusively) to refer to any of
+the three.
 
 \paragraph{Differences with old versions.}
 The current extraction mechanism is new for version 7.0 of {\Coq}.
@@ -21,7 +20,7 @@ In particular, the \FW\ toplevel used as an intermediate step between
 any more to import ML objects in this \FW\ toplevel.
 The current mechanism also differs from
 the one in previous versions of \Coq: there is no more
-an explicit toplevel for the language (formerly called {\sf Fml}). 
+an explicit toplevel for the language (formerly called \textsc{Fml}). 
 
 \asection{Generating ML code}
 \comindex{Extraction}
diff --git a/doc/Library.tex b/doc/Library.tex
index 35fda3ff7..7483e602c 100755
--- a/doc/Library.tex
+++ b/doc/Library.tex
@@ -48,7 +48,7 @@ The standard library is composed of the following subdirectories:
 \medskip
 
 Each of these subdirectories contains a set of modules, whose
-specifications ({\sf Gallina} files) have
+specifications (\gallina{} files) have
 been roughly, and automatically, pasted in the following pages. There
 is also a version of this document in HTML format on the WWW, which
 you can access from the \Coq\ home page at
diff --git a/doc/Makefile b/doc/Makefile
index 066d010bb..8ab0db0e9 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -30,7 +30,7 @@ TEST=test
 
 TEXINPUTS=/usr/local/lib/rrkit/RRINPUTSDIR:$(COQWEBSTY):$(HEVEALIB):.:
 
-INPUTS=./macros.tex ./title.tex ./headers.tex ./Reference-Manual.tex
+INPUTS=./version.tex ./macros.tex ./title.tex ./headers.tex ./Reference-Manual.tex
 
 LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \
          library/Wf.tex library/Specif.tex
@@ -51,10 +51,10 @@ REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
 
 REFMAN=Reference-Manual
 
-VERSION=V7.4
+VERSION=8.0
 #VERSION=POSITIONNEZ-CETTE-VARIABLE
 
-FTPDOCDIR=/net/pauillac/infosystems/ftp/coq/coq/$(VERSION)/doc
+FTPDOCDIR=/net/pauillac/infosystems/ftp/coq/coq/V$(VERSION)/doc
 WWWDOCDIR=/net/pauillac/infosystems/www/coq/doc
 
 FTPDOCS=Reference-Manual-base.ps.gz Reference-Manual-base.dvi.gz \
@@ -89,6 +89,9 @@ all-ps: Tutorial.v.ps Reference-Manual.ps # Library.ps Changes.v.ps
 
 all-html: Tutorial.v.html Reference-Manual.html # Library.html Changes.v.html
 
+#version
+version.tex: Makefile
+	echo "\newcommand{\coqversion}{$(VERSION)}" > version.tex
 
 #image coqide
 coqide.eps: coqide.png
diff --git a/doc/README b/doc/README
index f89d5c607..1693b1ca0 100755
--- a/doc/README
+++ b/doc/README
@@ -1,7 +1,7 @@
 You can get the whole documentation of Coq in the tar file all-ps-docs.tar.
 
 You can also get separately each document. The documentation of Coq
-V7.3 is divided into the following documents :
+V8.0 is divided into the following documents :
 
      * Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
 
@@ -31,7 +31,7 @@ V7.3 is divided into the following documents :
 
      * Library.ps: A description of the Coq standard library;
 
-     * CHANGES: A description of the differences between version 7.3
+     * CHANGES: A description of the differences between version 8.0
        and previous versions
 
      * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
diff --git a/doc/Recursive-Definition.tex b/doc/Recursive-Definition.tex
index 77774d9fa..6da37204f 100755
--- a/doc/Recursive-Definition.tex
+++ b/doc/Recursive-Definition.tex
@@ -2,7 +2,7 @@
 \input{title}
 
 \newcommand{\xx}{\noindent}
-\newcommand{\Coq}{{\sf Coq}}
+\newcommand{\Coq}{\textsc{Coq}}
 
 \begin{document}
 
@@ -101,13 +101,13 @@ function.
 \xx
 Such a proof is {\em automatically} synthesized by a
 {specialized strategy} which was originally designed for the
-{\sf ProPre} programming language. It has been adapted for
-the \Coq's framework. For a short description of the {\sf
-ProPre} programming language, we refer the reader to
+\textsc{ProPre} programming language. It has been adapted for
+the \Coq's framework. For a short description of the \textsc{ProPre}
+programming language, we refer the reader to 
 \cite{MPSI}. For details 
 concerning the original proof search strategy, we refer the
 reader to \cite{MSAR}. For theoretical settings of the
-method involved in {\sf ProPre}, we refer the reader to
+method involved in \textsc{ProPre}, we refer the reader to
 \cite{KRPA} and \cite{PARI}.
 
 \xx
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index f1eac15fd..55b4e71ad 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -1,4 +1,4 @@
-\chapter{Extensions of {\sf Gallina}}
+\chapter{Extensions of \Gallina{}}
 \label{Gallina-extension}\index{Gallina}
 
 {\gallina} is the kernel language of {\Coq}. We describe here extensions of
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index ec4a221d7..e27c729ce 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -1,4 +1,4 @@
-\chapter{The {\sf Gallina} specification language}
+\chapter{The \gallina{} specification language}
 \label{Gallina}\index{Gallina}
 
 This chapter describes \gallina, the specification language of Coq.
@@ -481,7 +481,7 @@ The expression {\tt CoFix} {\ident$_i$} \verb.{. \ident$_1$
 \ident$_n$ {\tt [} \binders$_n$ {\tt ] :} {\type$_n$}~\verb.}. denotes
 the $i$th component of a block of terms defined by a mutual guarded recursion. 
 
-\section{\em The Vernacular}
+\section{The Vernacular}
 \label{Vernacular}
 
 Figure \ref{sentences-syntax} describes {\em The Vernacular} which is the
diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
index a415dfb95..b610b7cc0 100644
--- a/doc/RefMan-ide.tex
+++ b/doc/RefMan-ide.tex
@@ -17,7 +17,7 @@ obviously no meaning for \coqide{} being ignored.
 
 \begin{figure}[t]
 \begin{center}
-\ifx\pdftexversion\undefined   % si on est pas en pdflatex
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
 \includegraphics[width=1.0\textwidth]{coqide.eps}
 \else
 \includegraphics[width=1.0\textwidth]{coqide.png}
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index a4e8445b1..0251a523c 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -1,7 +1,7 @@
 \setheaders{Introduction}
 \chapter*{Introduction}
 
-This document is the Reference Manual of version V7.1 of the \Coq\ 
+This document is the Reference Manual of version \coqversion{} of the \Coq\ 
 proof assistant. A companion volume, the \Coq\ Tutorial, is provided
 for the beginners. It is advised to read the Tutorial first.
 
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index 3e6f51a47..4b47c5028 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -337,7 +337,7 @@ reasoning and coercions in patterns.
 David Delahaye introduced a new language for tactics. General tactics
 using pattern-matching on goals and context can directly be written
 from the {\Coq} toplevel. He also provided primitives for the design
-of user-defined tactics in {\sf Caml}.
+of user-defined tactics in \textsc{Caml}.
 
 Micaela Mayero contributed the library on real numbers.
 Olivier Desmettre extended this library with axiomatic
@@ -345,7 +345,8 @@ trigonometric functions, square, square roots, finite sums, Chasles
 property and basic plane geometry.
 
 Jean-Christophe Filli�tre and Pierre Letouzey redesigned a new
-extraction procedure from {\Coq} terms to {\sf Caml} or {\sf Haskell} programs. This new
+extraction procedure from \Coq{} terms to \textsc{Caml} or
+\textsc{Haskell} programs. This new 
 extraction procedure, unlike the one implemented in previous version
 of \Coq{} is able to handle all terms in the Calculus of Inductive
 Constructions, even involving universes and strong elimination. P.
@@ -359,7 +360,7 @@ the confidence level in the correctness of {\Coq} critical type-checking
 algorithm.
 
 Yves Bertot designed  the \texttt{SearchPattern} and
-\texttt{SearchRewrite} tools and the support for the {\sf pcoq} interface 
+\texttt{SearchRewrite} tools and the support for the \textsc{pcoq} interface 
 (\url{http://www-sop.inria.fr/lemme/pcoq/}).
 
 Micaela Mayero and David Delahaye introduced {\tt Field}, a decision tactic for commutative fields.
@@ -454,11 +455,11 @@ integer numbers. Finally, the names of the standard properties of
 numbers now follow a standard scheme pattern and the symbolic
 notations for the standard definitions as well.
 
-The fourth point is the release of {\sf CoqIde} a new graphical
+The fourth point is the release of \CoqIde{}, a new graphical
 gtk2-based interface fully integrated to {\Coq}. Close in style from
 the Proof General Emacs interface, it is faster and its integration
 with {\Coq} makes interactive developments more friendly. All
-mathematical Unicode symbols are usable within {\sf CoqIde}.
+mathematical Unicode symbols are usable within \CoqIde{}.
 
 Finally, the module system of {\Coq} completes the picture of {\Coq}
 version 8.0. Tough released with an experimental status in the previous
@@ -487,7 +488,7 @@ tactic for solving first-order statements in presence of inductive
 types. He is also the maintainer of the non-domain specific automation
 tactics.
 
-Benjamin Monate is the developer of the {\sf CoqIde} graphical
+Benjamin Monate is the developer of the \CoqIde{} graphical
 interface.
 
 Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex
index ccba33b48..b812a3042 100755
--- a/doc/RefMan-uti.tex
+++ b/doc/RefMan-uti.tex
@@ -270,7 +270,7 @@ Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its
 specification (inductive types declarations, definitions, type of
 lemmas and theorems), removing the proofs parts of the file. The \Coq\
 file {\em file}{\tt.v} gives birth to the specification file
-{\em file}{\tt.g} (where the suffix {\tt.g} stands for {\sf Gallina}).
+{\em file}{\tt.g} (where the suffix {\tt.g} stands for \gallina).
 
 See the man page of {\tt gallina} for more details and options.
 
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 01dece65d..d4f4c4c76 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -1,28 +1,29 @@
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
 \documentclass[11pt,a4paper]{book}
+\else
+\documentclass[11pt,a4paper,pdftex]{book}
+\fi
+\usepackage[latin1]{inputenc}
 \usepackage[T1]{fontenc}
-%\usepackage[latin1]{inputenc}
+\usepackage{pslatex}
 \usepackage{url}
 \usepackage{verbatim}
-\usepackage{palatino}
-\usepackage{url}
+
 % for coqide
-\ifx\pdftexversion\undefined   % si on est pas en pdflatex
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
   \usepackage[dvips]{graphicx}
 \else
   \usepackage[pdftex]{graphicx}
 \fi
 
 
-\makeatletter
-
 %\includeonly{RefMan-cic.v,RefMan-ext.v}
 
+\input{./version.tex}
 \input{./macros.tex}% extension .tex pour htmlgen
 \input{./title.tex}% extension .tex pour htmlgen
 \input{./headers.tex}% extension .tex pour htmlgen
 
-\makeatother
-
 \begin{document}
 \tophtml{}
 \coverpage{Reference Manual}{The Coq Development Team}
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index 661169d6a..ef927764b 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -1,8 +1,9 @@
 \documentclass[11pt]{book}
 \usepackage[T1]{fontenc}
 \usepackage[latin1]{inputenc}
-\usepackage{palatino}
+\usepackage{pslatex}
 
+\input{./version.tex}
 \input{./macros.tex}
 \input{./title.tex}
 
@@ -31,8 +32,8 @@ that he calls \Coq~ from a standard teletype-like shell window, and that
 he does not use any special interface such as Emacs or Centaur. 
 Instructions on installation procedures, as well as more comprehensive
 documentation, may be found in the standard distribution of \Coq,
-which may be obtained by anonymous FTP from site \verb:ftp.inria.fr:,
-directory \verb:INRIA/coq/V7.4:. 
+which may be obtained by anonymous FTP from site \texttt{ftp.inria.fr},
+directory \texttt{INRIA/coq/V\coqversion}:. 
 
 In the following, all examples preceded by the prompting sequence
 \verb:Coq < : represent user input, terminated by a period. The
@@ -46,7 +47,7 @@ The standard invocation of \Coq\ delivers a message such as:
 \begin{flushleft}
 \begin{verbatim}
 unix:~> coqtop
-Welcome to Coq 7.4 (Feb 2003)
+Welcome to Coq 8.0 (Dec 2003)
 
 Coq < 
 \end{verbatim}
diff --git a/doc/biblio.bib b/doc/biblio.bib
index 06ef069d2..3e1d96344 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -120,10 +120,10 @@ s},
 
 @PhdThesis{Bou97These,
   author =       {S. Boutin},
-  title =        {R��flexions sur les quotients},
+  title =        {R\'eflexions sur les quotients},
   school =       {Paris 7},
   year =         1997,
-  type =         {th��se d'Universit��},
+  type =         {th\`ese d'Universit\'e},
   month =        apr
 }
 
@@ -166,7 +166,7 @@ s},
 
 @PHDTHESIS{CPar95,
         AUTHOR             = {C. Parent},
-        SCHOOL             = {Ecole {Normale} {Sup��rieure} de {Lyon}},
+        SCHOOL             = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
         TITLE              = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
         YEAR               = {1995}
 }
@@ -179,7 +179,7 @@ s},
 }
 
 @INPROCEEDINGS{ChiPotSimp03,
-  AUTHOR    = {Laurent Chicli and Lo�c Pottier and Carlos Simpson},
+  AUTHOR    = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson},
   ADDRESS   = {Berg en Dal, The Netherlands},
   TITLE     = {Mathematical Quotients and Quotient Types in Coq},
   BOOKTITLE = {TYPES'02},
@@ -229,7 +229,7 @@ s},
 @INPROCEEDINGS{CoPa89,
         AUTHOR             = {Th. Coquand and C. Paulin-Mohring},
         BOOKTITLE          = {Proceedings of Colog'88},
-        EDITOR             = {P. Martin-L��f and G. Mints},
+        EDITOR             = {P. Martin-L\"of and G. Mints},
         PUBLISHER          = {Springer-Verlag},
         SERIES             = {LNCS},
         TITLE              = {Inductively defined types},
@@ -299,15 +299,15 @@ s},
         AUTHOR             = {J. Courant},
         MONTH              = sep,
         SCHOOL             = {DEA d'Informatique, ENS Lyon},
-        TITLE              = {Explicitation de preuves par r��currence implicite},
+        TITLE              = {Explicitation de preuves par r\'ecurrence implicite},
         YEAR               = {1994}
 }
 
 @INPROCEEDINGS{Del99,
   author    = "Delahaye, D.",
-  title     = "Information {R}etrieval in a {{\sf Coq}} {P}roof {L}ibrary using
-               {T}ype {I}somorphisms",
-  booktitle = "Proceedings of TYPES'99, L��keberg",
+  title     = "Information Retrieval in a Coq Proof Library using
+               Type Isomorphisms",
+  booktitle = {Proceedings of TYPES'99, L\"okeberg},
   publisher = "Springer-Verlag LNCS",
   year      = "1999",
   url      =
@@ -332,9 +332,9 @@ s},
 
 @INPROCEEDINGS{DelMay01,
   author    = "Delahaye, D. and Mayero, M.",
-  title     = "{\tt Field}: une proc��dure de d��cision pour les nombres r��els
+  title     = "{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels
                en {{\sf Coq}}",
-  booktitle = "Journ��es Francophones des Langages Applicatifs, Pontarlier",
+  booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier",
   publisher = "INRIA",
   month     = "Janvier",
   year      = "2001",
@@ -511,7 +511,7 @@ s},
 }
 
 @TechReport{Gim98,
-  author = 	 {E. Gim��nez},
+  author = 	 {E. Gim\'enez},
   title = 	 {A Tutorial on Recursive Types in Coq},
   institution =  {INRIA},
   year = 	 1998,
diff --git a/doc/cover.html b/doc/cover.html
index 69e90d191..56063de89 100644
--- a/doc/cover.html
+++ b/doc/cover.html
@@ -19,14 +19,14 @@
 The Coq Proof Assistant<BR><BR>
  Reference Manual<BR></B></FONT><FONT SIZE=7>
 </FONT>
-<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 7.4</B></FONT><FONT SIZE=5><B>
+<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 8.0</B></FONT><FONT SIZE=5><B>
 </B></FONT><A NAME="text1"></A><A HREF="node.8.html#note1"><SUP><FONT SIZE=2>1</FONT></SUP></A><FONT SIZE=5><B><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 </B></FONT><FONT SIZE=5><B>The Coq Development Team</B></FONT><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>LogiCal Project</B></FONT><FONT SIZE=5><B><BR><BR><BR>
 </B></FONT></DIV><BR>
 <BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 
 <DIV ALIGN=left>
-<FONT SIZE=4>V7.4,
+<FONT SIZE=4>V8.0,
 </FONT><BR><FONT SIZE=4>�INRIA 1999-2003</FONT><BR></DIV>
 <BR>
 
diff --git a/doc/headers.tex b/doc/headers.tex
index 02b1e7e5c..f5b337340 100644
--- a/doc/headers.tex
+++ b/doc/headers.tex
@@ -29,6 +29,8 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % For the Addendum table of contents
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\makeatletter
+
 \newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
 \newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
 \newcommand{\achapter}[1]{
@@ -73,6 +75,9 @@ Vernacular Commands Index}
 \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
 \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
 \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
+\makeatother
+
+
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/macros.tex b/doc/macros.tex
index 5c22e72a9..2b2f0e1de 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -2,8 +2,6 @@
 % MACROS FOR THE REFERENCE MANUAL OF COQ %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\newcommand{\coqversion}{7.4}
-
 % For commentaries (define \com as {} for the release manual)
 %\newcommand{\com}[1]{{\it(* #1 *)}}
 \newcommand{\com}[1]{}
@@ -64,15 +62,16 @@
 % Trademarks and so on %
 %%%%%%%%%%%%%%%%%%%%%%%%
 
-\newcommand{\Coq}{{\sf Coq}}
+\newcommand{\Coq}{\textsc{Coq}}
+\newcommand{\gallina}{\textsc{Gallina}}
 \newcommand{\coqide}{\textsc{CoqIDE}}
-\newcommand{\ocaml}{{\sf Objective Caml}}
-\newcommand{\camlpppp}{{\sf Camlp4}}
-\newcommand{\emacs}{{\sf GNU Emacs}}
-\newcommand{\gallina}{\textsf{Gallina}}
-\newcommand{\CIC}{\mbox{\sc Cic}}
-\newcommand{\FW}{\mbox{$F_{\omega}$}}
-\newcommand{\bn}{{\sf BNF}}
+\newcommand{\CoqIde}{\textsc{CoqIDE}}
+\newcommand{\ocaml}{\textsc{Objective Caml}}
+\newcommand{\camlpppp}{\textsc{Camlp4}}
+\newcommand{\emacs}{\textsc{GNU Emacs}}
+\newcommand{\CIC}{\textsc{Cic}}
+\newcommand{\FW}{\ensuremath{F_{\omega}}}
+%\newcommand{\bn}{{\sf BNF}}
 
 %%%%%%%%%%%%%%%%%%%
 % Name of tactics %
diff --git a/doc/title.tex b/doc/title.tex
index 27651709a..4b643a727 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -49,7 +49,7 @@ Action ``Types''}
 \vspace*{520pt}
 \thispagestyle{empty}
 \begin{flushleft}
-{\large{V7.4,
+{\large{V\coqversion,
 \printingdate}}\\[20pt]
 {\large{\copyright INRIA 1999-2002}}\\
 \end{flushleft}