MAJ V7.1

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

5 files changed, 14 insertions, 747 deletions

diff --git a/doc/Changes.tex b/doc/Changes.tex
index 7b10f4f82..dec509651 100755
--- a/doc/Changes.tex
+++ b/doc/Changes.tex
@@ -8,742 +8,9 @@
 \begin{document}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Changes 6.3.1 ===> 7.0
+% Changes 6.3.1 ===> 7.0 & 7.1
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7}
-
-
-%This document describes the main differences between {\Coq} V6.3.1 and
-%V7. This new version of {\Coq} is characterized by fixed bugs, and
-%improvement of implicit arguments synthesis and speed in tactic
-%applications.
-
-\def\ltac{{\cal L}_{tac}}
-
-\section*{Overview}
-
-The new major version number is justified by a deep restructuration of
-the implementation code of \Coq. For the end-user, {\Coq}
-V7 provides the following novelties:
-
-\begin{itemize}
-\item A more high-level tactic language called $\ltac$ (see
-section~\ref{Tactics})
-\item A primitive let-in construction (see section \ref{Letin})
-which can also be used in \texttt{Record} definitions
-    (as suggested by Randy Pollack)
-\item Structuration of the developments in libraries and use of the
-dot notation to access names (see section \ref{Names})
-\item A search facilities by pattern
-provided by Yves Bertot (see section \ref{Search})
-\item A ``natural'' syntax for real numbers (see section
-\ref{SyntaxExtensions}) 
-\item New tactics (and developments) for real numbers 
-(see section~\ref{NewTactics})
-\item The tactic {\tt Field} which solves equalities using commutative field
-theory (see section~\ref{NewTactics})
-\item The tactic {\tt Fourier} to solve inequalities, developed by
-  Loïc Pottier has been integrated
-\item A command to export theories to XML to
-be used with Helm's publishing and rendering tools (see section
-\ref{XML})
-\item A new implementation of extraction (see section \ref{Extraction})
-%\item As usual, several bugs fixed and a lot of new ones introduced
-\end{itemize}
-
-Incompatibilities are described in section
-\ref{Incompatibilities}. Please notice that 
-{\tt Program/Realizer} is no more available in {\Coq} V7.
-
-Developers of tactics in ML are invited to read section
-\ref{Developers}.
-
-\paragraph{Changes between \Coq{} V7beta and \Coq{} V7}
-Some functionalities of \Coq{} V6.3 that were not available in \Coq{}
-V7beta has been restored~:
-\begin{itemize}
-\item A new mechanism for extraction of ML programs has been introduced.
-\item \texttt{Correctness} is now supported.
-\item Syntax for user-defined tactics calls does not require extra
-    parenthesis.
-\item \texttt{Elim} can be called even for non-inductive objects
-    when the apropriate elimination lemma exists.
-\item User defined tokens with arbitrary combination of letters and
-    symbols have been reintroduced.
-\end{itemize}
-\section{Language}
-\label{Language}
-\subsection{Primitive {\tt let ... in ...} construction}
-\label{Letin}
-The {\tt let ... in ...} syntax in V6.3.1 was implemented as a
-macro. It is now a first-class construction.
-
-\begin{coq_example}
-Require ZArith.
-Definition eight := [two:=`1 + 1`][four:=`two + two`]`four + four`. 
-Print eight.
-\end{coq_example}
-
-{\tt Local} definitions and {\tt Remark} inside a section now behaves
-as local definitions outside the section.
-
-\begin{coq_example}
-Section A.
-Local two := `1 + 1`.
-Definition four := `two + two`.
-End A.
-Print four.
-\end{coq_example}
-
-The unfolding of a reference with respect to a definition local to a section
-is performed by $\delta$ rule. But a ``{\tt let ... in ...}'' inside a term
-is not concerned by $\delta$ reduction. Commands to finely reduce this
-kind of expression remain to be provided.
-\medskip
-
-\paragraph{Alternative syntax}
- A less symbolic but equivalent syntax is available as~:\\ {\tt let
-two = `1 + 1` in `two + two`}.
-
-\paragraph{Local definitions in records}
-{\tt Local} definitions can be used inside record definitions as
-suggested by Randy Pollack~:
-\begin{coq_example}
-Record local_record : Set := {x:nat; y:=O; H:x=y}.
-Print local_record.
-Print x.
-Print y.
-Check H.
-\end{coq_example}
-
-\subsection{Libraries and qualified names}
-\label{Names}
-
-\paragraph{Identifiers} An identifier is any string beginning by a
-letter and followed by letters, digits or simple quotes. The bug
-with identifiers ended by a number greater than $2^{30}$ is fixed!
-
-\paragraph{Libraries}
-
-The theories developed in {\Coq} are now stored in {\it libraries}.  A
-library is characterized by a name called {\it root} of the
-library. By default, two libraries are defined at the beginning of a
-{\Coq} session. The first library has root name {\tt Coq} and contains the
-standard library of \Coq. The second has root name {\tt Scratch} and
-contains all definitions and theorems not explicitly put in a specific
-library. 
-
-Libraries have a tree structure. Typically, the {\tt Coq} library
-contains the (sub-)libraries {\tt Init}, {\tt Logic}, {\tt Arith},
-{\tt Lists}, ... The ``dot notation'' is used to write
-(sub-)libraries. Typically, the {\tt Arith} library of {\Coq} standard
-library is written ``{\tt Coq.Arith}''.
-
-\smallskip
-Remark: no space is allowed
-between the dot and the following identifier, otherwise the dot is
-interpreted as the final dot of the command!
-\smallskip
-
-Libraries and sublibraries can be mapped to physical directories of the
-operating system using the command
-
-\begin{quote}
-{\tt Add LoadPath {\it physical\_dir} as {\it (sub-)library}}.
-\end{quote}
-
-Incidentally, if a {\it (sub-)library} does not already
-exists, it is created by the command. This allows users to define new
-root libraries.
-
-A library can inherit the tree structure of a physical directory by
-using the command
-
-\begin{quote}
-{\tt Add Rec LoadPath {\it physical\_dir} as {\it (sub-)library}}.
-\end{quote}
-
-At some point, (sub-)libraries contain {\it modules} which coincides
-with files at the physical level. Modules themselves may contain
-sections, subsections, ... and eventually definitions and theorems.
-
-As for sublibraries, the dot notation is used to denote a specific
-module, section, definition or theorem of a library. Typically, {\tt
-Coq.Init.Logic.Equality.eq} denotes the Leibniz' equality defined in
-section {\tt Equality} of the module {\tt Logic} in the
-sublibrary {\tt Init} of the standard library of \Coq. By
-this way, a module, section, definition or theorem name is now unique
-in \Coq.
-
-\paragraph{Absolute and short names}
-
-The full name of a library, module, section, definition or theorem is
-called {\it absolute}. The final identifier {\tt eq} is called the
-{\it base name}. We call {\it short name} a name reduced to a single
-identifier.  {\Coq} maintains a {\it name table} mapping short names
-to absolute names. This greatly simplifies the notations and preserves
-compatibility with the previous versions of \Coq.
-
-\paragraph{Visibility and qualified names}
-An absolute path is called {\it visible} when its base name suffices
-to denote it. This means the base name is mapped to the absolute name
-in {\Coq} name table.
-
-All the base names of sublibraries, modules, sections, definitions and
-theorems are automatically put in the {\Coq} name table. But sometimes,
-names used in a module can hide names defined in another module.
-Instead of just distinguishing the clashing names by using the
-absolute names, it is enough to prefix the base name just by the name
-of its containing section (or module or library). 
-% CP : L'exemple avec Equality.eq ne semble pas fonctionner
-% E.g. if {\tt eq}
-% above is hidden by another definition of same base name, it is enough
-% to write {\tt Equality.eq} to access it... unless section {\tt
-% Equality} itself has been hidden in which case, it is necessary to
-% write {\tt Logic.Equality.eq} and so on. 
-Such a name built from
-single identifiers separated by dots is called a {\it qualified}
-name. Especially, both absolute names and short names are qualified
-names. Root names cannot be hidden in such a way fully qualified
-(i.e. absolute names) cannot be hidden.
-
-Examples:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example}
-Check O.
-Definition nat := bool.
-Check O.
-Check Datatypes.nat.
-\end{coq_example}
-
-\paragraph{Requiring a file}
-
-When a ``.vo'' file is required in a physical directory mapped to some
-(sub-)library, it is adequately mapped in the whole library structure
-known by \Coq. However, no consistency check is currently done to
-ensure the required module has actually been compiled with the same
-absolute name (e.g. a module can be compiled with absolute name
-{\tt Mycontrib.Arith.Plus} but required with absolute name
-{\tt HisContrib.ZArith.Plus}).
-
-The command {\tt Add Rec LoadPath} is also available from {\tt coqtop}
-and {\tt coqc} by using option \verb=-R= (see section \ref{Tools}).
-
-\subsection{Syntax extensions}
-\label{SyntaxExtensions}
-
-\paragraph{``Natural'' syntax for real numbers}
-A ``natural'' syntax for real numbers and operations on reals is now
-available by putting expressions inside pairs of backquotes.
-
-\begin{coq_example}
-Require Reals.
-Check ``2*3/(4+2)``.
-\end{coq_example}
-Remark: A constant, say \verb:``4``:, is equivalent to
-\verb:``(1+(1+(1+1)))``:.
-
-\paragraph{{\tt Infix}} was inactive on pretty-printer. Now it works.
-
-\paragraph{Consecutive symbols} are now considered as an unique token.
-Exceptions have been coded in the lexer to separate tokens we do not want to
-separate (for example \verb:A->~B:), but this is not exhaustive and some spaces
-may have to be inserted in some cases which have not been treated
-(e.g. \verb:~<nat>O=O: should now be written \verb:~ <nat>O=O:).
-
-%should now be separated (e.g. by a
-%space). Typically, the string \verb:A->~<nat>O=O: is no longer
-%recognized. It should be written \verb:A-> ~ <nat>O=O:... or simply
-%\verb:A->~ <nat>O=O: because of a special treatment for \verb:->:!
-
-\paragraph{The {\tt command} syntactic class for {\tt Grammar}} has
-been renamed {\tt constr} consistently with the usage for {\tt Syntax}
-extensions. Entries {\tt command1}, {\tt command2}, ... are renamed
-accordingly. The type {\tt List} in {\tt Grammar} rules has been
-renamed {\tt ast list}.
-
-\paragraph{Default parser in {\tt Grammar} and {\tt Syntax}}
-\label{GrammarSyntax}
-
-The default parser for right-hand-side of {\tt Grammar} rules and for
-left-hand-side of {\tt Syntax} rule was the {\tt ast} parser.  Now it
-is the one of same name as the syntactic class extended (i.e. {\tt
-constr}, {\tt tactic} or {\tt vernac}). As a consequence, 
-{\verb:<< ... >>:} should be removed.
-
-On the opposite, in rules expecting the {\tt ast} parser,
-{\verb:<< ... >>:} should be added in the left-hand-side of {\tt Syntax} rule.
-As for {\tt Grammar} rule, a typing constraint, {\tt ast} or {\tt ast
-list} needs to be explicitly given to force the use of the {\tt ast}
-parser. For {\tt Grammar} rule building a new syntactic class,
-different from {\tt constr}, {\tt tactic}, {\tt vernac} or {\tt ast},
-any of the previous keyword can be used as type (and therefore as
-parser).
-
-See examples in appendix.
-
-\paragraph{Syntax overloading}
-
- Binding of constructions in Grammar rules is now done with absolute
-  paths. This means overloading of syntax for different constructions
-  having the same base name is no longer possible.
-
-\paragraph{Timing or abbreviating a sequence of commands}
-
-The syntax {\tt [ {\it phrase$_1$} ... {\it phrase$_n$} ].} is now
-available to group several commands into a single one (useful for
-{\tt Time} or for grammar extensions abbreviating sequence of commands).
-
-\subsection{Miscellaneous}
-
-\paragraph{Pattern aliases} of dependent type in \verb=Cases=
-expressions are currently not supported.
-
-\subsection{Libraries}
-The names of directories in \texttt{theories} has been changed. The
-directory \texttt{theories/Zarith} has been renamed
-\texttt{theories/ZArith} between \Coq{} V7.0beta and V7.0.
-
-A new directory \texttt{theories/IntMap} has been added which
-contains an efficient representation of finite sets 
-as maps indexed by binary integers. This development has been
-developed by J. Goubault and was previously an external contribution.
-
-Some definitions, lemmas and theorems have been added or reorganised,
-see the Library documentation for more information.
-
-\section{Tactics}
-\label{Tactics}
-\def\oc{{\sf Objective~Caml}}
-
-\subsection{A tactic language: $\ltac$}
-
-$\ltac$ is a new layer of metalanguage to write tactics and especially to deal
-with small automations for which the use of the full programmable metalanguage
-(\oc{}) would be excessive. $\ltac$ is mainly a small functional core with
-recursors and elaborated matching operators for terms but also for proof
-contexts. This language can be directly used in proof scripts or in toplevel
-definitions ({\tt Tactic~Definition}). It has been noticed that non-trivial
-tactics can be written with $\ltac$ and to provide a Turing-complete
-programming framework, a quotation has been built to use $\ltac$ in \oc{}.
-$\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/}
-
-\paragraph{Tactic debugger}
-
-  \paragraph{{\tt Debug $($ On $|$ Off $)$}} turns on/off the tactic
-  debugger for $\ltac$.
-  This is still very experimental and no documentation is provided yet.
-
-
-\subsection{New tactics}
-\label{NewTactics}
-\def\ml{{\sf ML}}
-
-   \paragraph{{\tt Field}} written by David~Delahaye and Micaela~Mayero solves
-equalities using commutative field theory. This tactic is reflexive and has
-been implemented using essentially the new tactic language $\ltac$. Only the
-table of field theories (as for the tactic {\tt Ring}) is dealt by means of an
-\ml{} part. This tactic is currently used in the real number theory. For more
-details, see the Reference Manual.
-
-   \paragraph{{\tt Fourier}} written by Loïc Pottier solves linear inequations.
-
-   \paragraph{Other tactics and developments} has been included in the real
-numbers library: {\tt DiscrR} proves that a real integer constant $c_1$ is non 
-equal to another real integer constant $c_2$; {\tt SplitAbsolu} allows us to 
-unfold {\tt Rabsolu} contants and split corresponding conjonctions; 
-{\tt SplitRmult} allows us to split a condition that a product is non equal to 
-zero into subgoals corresponding to the condition on each subterm of the 
-product. All these tactics have been written with the tactic language 
-$\ltac$.\\ 
-A development on Cauchy series, power series,... has been also added.\\
-For more details, see the Reference Manual.
-
-\subsection{Changes in pre-existing tactics}
-\label{TacticChanges}
-
-   \paragraph{{\tt Tauto} and {\tt Intuition}} have been rewritten using the
-   new tactic language $\ltac$. The code is now quite shorter and a significant
-   increase in performances has been noticed. {\tt Tauto} has exactly the same
-   behavior. {\tt Intuition} is slightly less powerful (w.r.t. to dependent
-   types which are now considered as atomic formulas) but it has clearer
-   semantics. This may lead to some incompatibilities.
-
-  \paragraph{{\tt Simpl}} now simplifies mutually defined fixpoints
-  as expected (i.e. it does not introduce {\tt Fix id
-  \{...\}} expressions).
-
-  \paragraph{{\tt AutoRewrite}} now applies only on main goal and the remaining
-  subgoals are handled by\break{}{\tt Hint~Rewrite}. The syntax is now:\\
-
-  {\tt Hint Rewrite $($ -> $|$ <- $)*$ [ $term_1$ $...$ $term_n$ ] in
-    $ident$ using $tac$}\\
-
-  Adds the terms $term_1$ $...$ $term_n$ (their types must be equalities) in
-  the rewriting database $ident$ with the corresponding orientation (given by
-  the arrows; default is left to right) and the tactic $tac$ which is applied
-  to the subgoals generated by a rewriting, the main subgoal excluded.\\
-
-  {\tt AutoRewrite  [ $ident_1$ $...$ $ident_n$ ] using $tac$}\\
-
-  Performs all the rewritings given by the databases $ident_1$ $...$ $ident_n$
-  applying $tac$ to the main subgoal after each rewriting step.\\
-
-  See the contribution \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} for
-  examples.
-
-  \paragraph{{\tt Intro $hyp$} and {\bf \tt Intros $hyp_1$ ... $hyp_n$}}
-  now fail if the hypothesis/variable name provided already exists.
-
-  \paragraph{{\tt Prolog}} is now part of the core
-  system. Don't use {\tt Require Prolog}.
-
-  \paragraph{{\tt Unfold}} now fails when its argument is not an
-  unfoldable constant.
-
-  \paragraph{Tactic {\tt Let}} has been renamed into {\tt LetTac}
-  and it now relies on the primitive {\tt let-in} constructions
-
-  \paragraph{{\tt Apply ... with ...}} when instantiations are
-  redundant or incompatible now behaves smoothly.
-
-  \paragraph{{\tt Decompose}} has now less bugs. Also hypotheses
-  are now numbered in order.
-
-  \paragraph{{\tt Linear}} seems to be very rarely used. It has not
-  been ported in {\Coq} V7.
-
-  \paragraph{{\tt Program/Realizer}} has not been ported in {\Coq} V7.
-
-\section{Toplevel commands}
-
-\subsection{Searching the environment}
-\label{Search}
-A new searching mechanism by pattern has been contributed by Yves Bertot.
-
-
-\paragraph{{\tt SearchPattern {\term}}}
-displays the name and type of all theorems of the current
-context whose statement's conclusion matches the expression {\term}
-where holes in the latter are denoted by ``{\tt ?}''.
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Require Arith.
-SearchPattern (plus ? ?)=?.
-\end{coq_example}
-
-Patterns need not be linear: you can express that the same
-expression must occur in two places by using indexed ``{\tt ?}''.
-
-\begin{coq_example}
-Require Arith.
-SearchPattern (plus ? ?1)=(mult ?1 ?).
-\end{coq_example}
-
-\paragraph{{\tt SearchRewrite {\term}}}
-displays the name and type of all theorems of the current
-context whose statement's conclusion is an equality of which one side matches
-the expression {\term}. Holes in {\term} are denoted by ``{\tt ?}''.
-
-\begin{coq_example}
-Require Arith.
-SearchRewrite (plus ? (plus ? ?)).
-\end{coq_example}
-
-\begin{Variants}
-
-\item {\tt SearchPattern {\term} inside {\module$_1$}...{\module$_n$}}\\
-{\tt SearchRewrite {\term} inside
-{\module$_1$}...{\module$_n$}.}
-
-  This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
-
-\item {\tt SearchPattern {\term} outside {\module}.}\\
-{\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}
-
-  This restricts the search to constructions not defined in modules {\module$_1$}...{\module$_n$}.
-
-\end{Variants}
-
-\paragraph{{\tt Search {\ident}.}} has been extended to accept qualified
-identifiers and the {\tt inside} and {\tt outside} restrictions as
-{\tt SearchPattern} and {\tt SearchRewrite}.
-
-\paragraph{{\tt SearchIsos {\term}.}} has not been ported yet.
-
-\subsection{XML output}
-\label{XML}
-
-A printer of {\Coq} theories into XML syntax has been contributed by
-Claudio Sacerdoti Coen. Various printing commands (such as {\tt Print
-XML Module {\ident}}) allow to produce XML files from
-``.vo'' files. In order to experiment these possibilities, you need to
-require the \Coq{} \texttt{Xml} module first.
-
-These XML files can be published on the Web, retrieved
-and rendered by tools developed in the HELM project (see
-http://www.cs.unibo.it/helm).
-
-\subsection{Other new commands}
-
-
-  \paragraph{{\tt Implicits {\ident}}} associate to \ident{}  
-  implicit arguments as if the implicit arguments mode was on.
-
-  \paragraph{{\tt Implicits {\ident} [{\num} \ldots {\num}]}}
-        allows to explicitly give what arguments
-        have to be considered as implicit in {\ident}.
-
-\begin{coq_example}
-Parameter exists : (A:Set)(P:A->Prop)(x:A)(P x)->(EX x:A |(P x)).
-Implicits exists.
-Print exists.
-Implicits exists [1].
-Print exists.
-\end{coq_example}
-
-\subsection{Syntax standardisation}
-
-The commands on the left are now equivalent to (old) commands on
-the right.
-
-\medskip
-
-\begin{tt}
-\begin{tabular}{ll}
-Set Implicit Arguments & Implicit Arguments On \\
-Unset Implicit Arguments ~~~~~ & Implicit Arguments Off \\
-Add LoadPath & AddPath \\
-Add Rec LoadPath & AddRecPath \\
-Remove LoadPath & DelPath \\
-Set Silent & Begin Silent \\
-Unset Silent & End Silent \\
-Print Coercion Paths & Print Path\\
-\end{tabular}
-\end{tt}
-
-\medskip
-
-Commands on the right remains available for compatibility reasons (except for
-{\tt Begin Silent} and {\tt End Silent} which interfere with
-section closing, and for the misunderstandable {\tt Print Path}).
-
-\subsection{Other Changes}
-
-
-\paragraph{Final dot} Commands should now be ended by a final dot ``.'' followed by a blank
-(space, return, line feed or tabulation). This is to distinguish from
-the dot notation for qualified names where the dot must immediately be
-followed by a letter (see section \ref{Names}).
-
-\paragraph{Eval Cbv Delta ... in ...} The {\tt [- {\it
-const}]}, if any, should now immediately follow the {\tt Delta} keyword.
-
-
-\section{Tools}
-\label{Tools}
-
-\paragraph{Consistency check for {\tt .vo} files} A check-sum test
-avoids to require inconsistent {\tt .vo} files.
-
-\paragraph{Optimal compiler} If your architecture supports it, the native
-version of {\tt coqtop} and {\tt coqc} is used by default.
-
-\paragraph{Option -R} The {\tt -R} option to {\tt coqtop} and {\tt
-coqc} now serves to link physical path to logical paths (see
-\ref{Names}). It expects two arguments, the first being the physical
-path and the second its logical alias. It still recursively scans
-subdirectories.
-
-\paragraph{Makefile automatic generation} {\tt coq\_makefile} is the
-new name for {\tt do\_Makefile}.
-
-\paragraph{Error localisation} Several kind of typing errors are now
-located in the source file.
-
-\section{Extraction}\label{Extraction}
-Extraction code has been completely rewritten by J.-C. Filliâtre and
-P. Letouzey since version V6.3. 
-This work is still not finished, but most parts of it are already
-usable. It was successfully tested on the \Coq{} theories.
-
-The new mechanism is able to extract programs from any \Coq{} term
-(including terms at the Type level). 
-A new mechanism to extract Ocaml modules from Coq files has been
-added. 
-
-However, the resulting ML term is not guaranteed to be typable in ML
-(the next version should incorporate automatically appropriate conversions).
-
-Only extraction towards Ocaml programs is currently available. 
-The \verb=ML import= command is not available anymore, the command
-\verb=Extract Constant=  can be used to realize a \Coq{} axiom by 
-an ML program.
-
-More
-information can be found in \verb=$COQTOP/contrib/extraction/README=. 
-The syntax of commands is described in the Reference Manual.
-
-
-\section{Developers}
-\label{Developers}
-The internals of {\Coq} has changed a lot and will continue to change
-significantly in the next months. We recommend tactic developers to
-take contact with us for adapting their code. A document describing
-the interfaces of the ML modules constituting {\Coq} is available
-thanks to J.-C. Filliatre's ocamlweb
-documentation tool (see the ``doc'' directory in {\Coq} source).
-
-\section{Incompatibilities}
-\label{Incompatibilities}
-
-  You could have to modify your vernacular source for the following
-  reasons:
-
-  \begin{itemize}
- 
-  \item Any of the tactic changes mentioned in section \ref{TacticChanges}.
-
-  \item The ``.vo'' files are not compatible and all ``.v'' files should
-  be recompiled.
-
-  \item Consecutive symbols may have to be separated in some cases (see
-  section~\ref{SyntaxExtensions}).
-
-  \item Default parsers in {\tt Grammar} and {\tt Syntax} are
-  different (see section \ref{GrammarSyntax}).
-  
-  \item Definition of {\tt D\_in} (Rderiv.v) is now with Rdiv and not 
-        with Rmult and Rinv as before.
-
-  \item Pattern aliases of dependent type in \verb=Cases=
-        expressions are currently not supported.
-
-  \end{itemize}
-
-A shell script \verb=translate_V6-3-1_to_V7= is available in the archive to
-automatically translate V6.3.1 ``.v'' files to V7.0 syntax
-(incompatibilities due to changes in tactics semantics are not
-treated).
-
-%\section{New users contributions}
-
-\section{Installation procedure}
-
-%\subsection{Operating System Issues -- Requirements}
-
-{\Coq} is available as a source package at 
-
-\begin{quote}
-\verb|ftp://ftp.inria.fr/INRIA/coq/V7|\\
-\verb|http://coq.inria.fr|
-\end{quote}
-
-You need Objective Caml version 3.00 or later, and the corresponding 
-Camlp4 version to compile the system. Both are available by anonymous ftp
-at:
-
-\begin{quote}
-\verb|ftp://ftp.inria.fr/Projects/Cristal|\\
-\verb|http://caml.inria.fr|
-\end{quote}
-
-\noindent
-%Binary distributions are available for the following architectures:
-%
-%\bigskip
-%\begin{tabular}{l|c|r}
-%{\bf OS } & {\bf Processor} & {name of the package}\\
-%\hline
-%Linux & 80386 and higher & coq-6.3.1-Linux-i386.tar.gz \\
-%Solaris & Sparc & coq-6.3.1-solaris-sparc.tar.gz\\
-%Digital & Alpha & coq-6.3.1-OSF1-alpha.tar.gz\\
-%\end{tabular}
-%\bigskip
-
-%A rpm package is available for i386 Linux users. No other binary
-%package is available for this beta release.
-
-%\bigskip
-%
-%If your configuration is in the above list, you don't need to install
-%Caml and Camlp4 and to compile the system: 
-%just download the package and install the binaries in the right place.
-
-%\paragraph{MS Windows users}
-%
-%A binary distribution is available for PC under MS Windows 95/98/NT.
-%The package is named coq-6.3.1-win.zip.
-%
-%For installation information see the 
-%files INSTALL.win and README.win.
-
-\section*{Appendix}
-\label{Appendix}
-We detail the differences between {\Coq} V6.3.1 and V7.0 for the {\tt
-Syntax} and {\tt Grammar} default parsers.
-
-\medskip
-
-{\bf Examples in V6.3.1}
-
-\begin{verbatim}
-Grammar command command0 :=
-  pair [ "(" lcommand($lc1) "," lcommand($lc2) ")" ] ->
-         [<<(pair ? ? $lc1 $lc2)>>].
-
-Syntax constr
-  level 1:
-  pair [<<(pair $_ $_ $t3 $t4)>>] -> [[<hov 0> "(" $t3:E ","[0 1] $t4:E ")" ]].
-
-Grammar znatural formula :=
-  form_expr [ expr($p) ] -> [$p]
-| form_eq [ expr($p) "=" expr($c) ] -> [<<(eq Z $p $c)>>].
-
-Syntax constr
-  level 0:
-    Zeq [<<(eq Z $n1 $n2)>>] -> 
-      [[<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]].
-
-Grammar tactic simple_tactic :=
-  tauto [ "Tauto" ] -> [(Tauto)].
-\end{verbatim}
-
-\medskip
-
-{\bf New form in V7.0beta}
-
-\begin{verbatim}
-Grammar constr constr0 :=
-  pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] -> [ (pair ? ? $lc1 $lc2) ].
-
-Syntax constr
-  level 1:
-    pair [ (pair $_ $_ $t3 $t4) ] -> [[<hov 0> "(" $t3:E ","[0 1] $t4:E ")" ]].
-
-Grammar znatural formula : constr :=
-  form_expr [ expr($p) ] -> [ $p ]
-| form_eq [ expr($p) "=" expr($c) ] -> [ (eq Z $p $c) ].
-
-Syntax constr
- level 0:
-  Zeq [ (eq Z $n1 $n2) ] -> 
-    [<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]].
-
-Grammar tactic simple_tactic: ast :=
-  tauto [ "Tauto" ] -> [(Tauto)].
-\end{verbatim}
+\shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7.0 and V7.1}
 
 \end{document}
 
diff --git a/doc/RefMan-cover.tex b/doc/RefMan-cover.tex
index 2fdde9357..d881329a6 100644
--- a/doc/RefMan-cover.tex
+++ b/doc/RefMan-cover.tex
@@ -2,8 +2,8 @@
         % L'utilisation du style `french' force le résumé français à
         % apparaître en premier.
 
-\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.0}
-\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.0
+\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1}
+\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1
 \thanks
 {This research was partly supported by ESPRIT Basic Research
 Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
@@ -14,7 +14,7 @@ Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy,
 Catherine Parent, Christine Paulin-Mohring,
 Amokrane Sa{\"\i}bi, Benjamin Werner}
 \authorhead{}
-\titlehead{Coq V7.0 Reference Manual}
+\titlehead{Coq V7.1 Reference Manual}
 \RRtheme{2}
 \RRprojet{Coq}
 \RRNo{0123456789}
@@ -25,7 +25,7 @@ Amokrane Sa{\"\i}bi, Benjamin Werner}
 \RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
 v\'erification de preuves formelles dans une logique d'ordre
 sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
-Ce document constitue le manuel de r\'ef\'erence de la version V7.0
+Ce document constitue le manuel de r\'ef\'erence de la version V7.1
 qui est distribu\'ee par ftp anonyme à l'adresse
 \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
@@ -35,7 +35,7 @@ Calcul des Constructions Inductives}
 
 \RRabstract{Coq is a proof assistant based on a higher-order logic
 allowing powerful definitions of functions. 
-Coq V7.0 is available by anonymous
+Coq V7.1 is available by anonymous
 ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
diff --git a/doc/Tutorial-cover.tex b/doc/Tutorial-cover.tex
index 1acd7d084..b747b812e 100644
--- a/doc/Tutorial-cover.tex
+++ b/doc/Tutorial-cover.tex
@@ -2,11 +2,11 @@
         % L'utilisation du style `french' force le résumé français à
         % apparaître en premier.
 \RRetitle{
-The Coq Proof Assistant \\ A Tutorial \\ Version 7.0
+The Coq Proof Assistant \\ A Tutorial \\ Version 7.1
 \thanks{This research was partly supported by ESPRIT Basic Research
 Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
 }
-\RRtitle{Coq \\ Une introduction \\ V7.0 }
+\RRtitle{Coq \\ Une introduction \\ V7.1 }
 \RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring}
 \RRtheme{2}
 \RRprojet{{Coq
@@ -29,7 +29,7 @@ Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNR
 v\'erification de preuves formelles dans une logique d'ordre
 sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
 Ce document constitue une introduction pratique \`a l'utilisation de
-la version V7.0 qui est distribu\'ee par ftp anonyme à l'adresse
+la version V7.1 qui est distribu\'ee par ftp anonyme à l'adresse
 \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul
@@ -37,7 +37,7 @@ des Constructions Inductives}
 
 \RRabstract{Coq is a proof assistant based on a higher-order logic
 allowing powerful definitions of functions. This document is a
-tutorial for the version V7.0 of Coq. This version is available by
+tutorial for the version V7.1 of Coq. This version is available by
 anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
diff --git a/doc/cover.html b/doc/cover.html
index cb87ed106..2391dbeaf 100644
--- a/doc/cover.html
+++ b/doc/cover.html
@@ -25,7 +25,7 @@ The Coq Proof Assistant<BR><BR>
 <BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 
 <DIV ALIGN=left>
-<FONT SIZE=4>V7.0,
+<FONT SIZE=4>V7.1,
 </FONT><BR><FONT SIZE=4>©INRIA 1999-2001</FONT><BR></DIV>
 <BR>
 
@@ -36,4 +36,4 @@ The Coq Proof Assistant<BR><BR>
 
 </HTML></BODY>
 
-</HTML>
\ No newline at end of file
+</HTML>
diff --git a/doc/title.tex b/doc/title.tex
index f9051a1b3..28165c0df 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -49,7 +49,7 @@ Action ``Types''}
 \vspace*{520pt}
 \thispagestyle{empty}
 \begin{flushleft}
-{\large{V7.0,
+{\large{V7.1,
 \printingdate}}\\[20pt]
 {\large{\copyright INRIA 1999-2001}}\\
 \end{flushleft}