blob: 4eac45633895e040ace29da78826e0de18744609 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
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$
|
