\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$