diff options
author | 2003-12-01 15:40:29 +0000 | |
---|---|---|
committer | 2003-12-01 15:40:29 +0000 | |
commit | 8b827e1540166eed6cdd8f603eb9eb1a5e42ec84 (patch) | |
tree | b09cf6cb624c8cd1ddeaa3d234b795a2ac272214 | |
parent | bc73bc1ef78f6cb5cabb173e633be9cc96a05180 (diff) |
version et style
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8371 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/.cvsignore | 1 | ||||
-rwxr-xr-x | doc/Anomalies.tex | 2 | ||||
-rwxr-xr-x | doc/ChangesV7-0.tex | 6 | ||||
-rwxr-xr-x | doc/Extraction.tex | 15 | ||||
-rwxr-xr-x | doc/Library.tex | 2 | ||||
-rw-r--r-- | doc/Makefile | 9 | ||||
-rwxr-xr-x | doc/README | 4 | ||||
-rwxr-xr-x | doc/Recursive-Definition.tex | 10 | ||||
-rw-r--r-- | doc/RefMan-ext.tex | 2 | ||||
-rw-r--r-- | doc/RefMan-gal.tex | 4 | ||||
-rw-r--r-- | doc/RefMan-ide.tex | 2 | ||||
-rwxr-xr-x | doc/RefMan-int.tex | 2 | ||||
-rwxr-xr-x | doc/RefMan-pre.tex | 13 | ||||
-rwxr-xr-x | doc/RefMan-uti.tex | 2 | ||||
-rw-r--r-- | doc/Reference-Manual.tex | 17 | ||||
-rwxr-xr-x | doc/Tutorial.tex | 9 | ||||
-rwxr-xr-x | doc/biblio.bib | 24 | ||||
-rw-r--r-- | doc/cover.html | 4 | ||||
-rw-r--r-- | doc/headers.tex | 5 | ||||
-rwxr-xr-x | doc/macros.tex | 19 | ||||
-rwxr-xr-x | doc/title.tex | 2 |
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} |