aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Changes.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/Changes.tex')
-rwxr-xr-xdoc/Changes.tex160
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$
+