diff options
Diffstat (limited to 'doc/ChangesV7-0.tex')
| -rwxr-xr-x | doc/ChangesV7-0.tex | 757 |
1 files changed, 0 insertions, 757 deletions
diff --git a/doc/ChangesV7-0.tex b/doc/ChangesV7-0.tex deleted file mode 100755 index b593b9dc8..000000000 --- a/doc/ChangesV7-0.tex +++ /dev/null @@ -1,757 +0,0 @@ -\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$ - |