Pr�c�dent Changes.tex

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

1 files changed, 757 insertions, 0 deletions

diff --git a/doc/ChangesV7-0.tex b/doc/ChangesV7-0.tex
new file mode 100755
index 0000000000..7b10f4f825
--- /dev/null
+++ b/doc/ChangesV7-0.tex
@@ -0,0 +1,757 @@
+\documentclass[11pt]{article}
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+
+\input{./title}
+\input{./macros}
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Changes 6.3.1 ===> 7.0
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\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}
+
+\end{document}
+
+% Local Variables: 
+% mode: LaTeX
+% TeX-master: t
+% End: 
+
+
+% $Id$ 
+