diff options
Diffstat (limited to 'doc/Changes.tex')
-rwxr-xr-x | doc/Changes.tex | 160 |
1 files changed, 160 insertions, 0 deletions
diff --git a/doc/Changes.tex b/doc/Changes.tex new file mode 100755 index 000000000..4eac45633 --- /dev/null +++ b/doc/Changes.tex @@ -0,0 +1,160 @@ +\documentclass[11pt]{article} +\usepackage[latin1]{inputenc} +\usepackage[T1]{fontenc} + +\input{./title} +\input{./macros} + +\begin{document} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Changes 6.3 ===> 6.3.1 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\shorttitle{Changes from {\Coq} V6.3 to {\Coq} V6.3.1} + +This document describes the main differences between Coq V6.3 and +V6.3.1. This new version of Coq is characterized by fixed bugs, and +improvement of implicit arguments synthesis and speed in tactic +applications. + +\section{Changes overview} + +\subsection{Tactics} + + \begin{itemize} + + \item \texttt {Tauto} has been unable for a time to deal with +hypotheses with 2 imbricated implications. Now it should work. +\texttt {Intuition} now removes true, and therefore useless, +hypotheses.\\ + + \item Several bugs of the {\texttt Program} are fixed (but some + automatically generated names have changed and may lead to + incompatibilities). + + \item Bug with negative index in bindings fixed. + + \item Speed improvement: redondant checks when applying a tactic + have been turned off. For some tactics that don't make themselves + the expected verifications, it may result in incorrect proofs + detected only at Qed/Save time. In this last case, you can turn on + the -tac-debug flag to coqtop. + + \item The ``?'' in goals are now instantiated as soon as an instance + is known for them. + + \end{itemize} + +\subsection{Toplevel commands} + +\begin{description} + +\item Bug in \texttt{Time} fixed. + +\end{description} + +\subsection{Language} + + \begin{description} \item[Type reconstruction] The algorithm to + solve incomplete information in terms has been improved + furthermore. In particular question marks can be put in in place of + the type of abstracted variables and in Cases expressions. + + \item[Guarded cofixpoints] A weakness in the guardness condition + when a cofixpoint refers to another one has been corrected. + WARNING: the new criterion may refuse some olderly accepted + Cofixpoint definitions which actually are valid but for a reason + difficult to detect automatically. + + \item[Extraction] A bug was limiting the number of propositional + singleton inductive types (such has ``eq'') for which elimination + towards Set is valid. + + \end{description} + +\subsection{Incompatibilities} + + You could have to modify your vernacular source for the following + reasons: + + \begin{itemize} + + \item Some names of variables generated by the \texttt{Program} have + changed. + + \item {\texttt Intuition} now remove trye hypotheses. + + \item In all cases, the ``.vo'' files are not compatible and should + be recompiled. + + \end{itemize} + +\section{New users contributions} + + \begin{description} + + \item[Binary Decision Diagrams] provided by Kumar Verma (Dyade) + + \item[A distributed reference counter] (part of a + garbage collector) provided by Jean Duprat (ENS-Lyon) + +\end{description} + +\section{Installation procedure} + +\subsection{Uninstalling Coq} + +\paragraph{Warning} +It is strongly recommended to clean-up the V6.3 Coq library directory +before you install the new version. +Use the option to coqtop \texttt{-uninstall} that will remove +the binaries and the library files of Coq V6.3 on a Unix system. + +\subsection{OS Issues -- Requirements} + +\subsubsection{Unix users} +You need Objective Caml version 2.01 or later, and the corresponding +Camlp4 version to compile the system. Both are available by anonymous ftp +at: \\ +\verb|ftp://ftp.inria.fr/Projects/Cristal|. +\bigskip + +\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 + +There is also rpm packages for Linux. + +\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. + +\subsubsection{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. + +\end{document} + +% Local Variables: +% mode: LaTeX +% TeX-master: t +% End: + + +% $Id$ + |