path: root/doc/ChangesV7-0.tex

\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{\textsc{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:\\

\url{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{\textsc{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$