diff options
Diffstat (limited to 'doc/ChangesV6-3-1.tex')
| -rw-r--r-- | doc/ChangesV6-3-1.tex | 160 |
1 files changed, 0 insertions, 160 deletions
diff --git a/doc/ChangesV6-3-1.tex b/doc/ChangesV6-3-1.tex deleted file mode 100644 index 4eac45633..000000000 --- a/doc/ChangesV6-3-1.tex +++ /dev/null @@ -1,160 +0,0 @@ -\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$ - |