blob: a21577db0e108a184ed9741e213e644896f2524d (
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
|
\documentclass[11pt]{article}
\input{./title}
\title{Known bugs of \Coq{} V6.2}
\author{\ }
\begin{document}
\maketitle
\begin{itemize}
\item {\tt Program} may fail to build pattern in {\tt Cases}
expressions. Instead an old style {\tt Case} expression without
patterns is generated.
\item The option {\tt Set Printing Synth} sometimes fails to decide if
a elimination predicates is synthetisable. If a term printed without
the elimination predicate is not correctly re-interpreted by Coq, then
turn off the {\tt Printing Synth} mode.
\item {\tt Unfold} and {\tt Pattern} may incorrectly number the
occurrences of constants or subterms when {\tt Cases} expression are involved.
\item \texttt{Transparent} and \texttt{Opaque} are not synchronous
with the \texttt{Reset} mecanism. If a constant was transparent at
point \texttt{A}, if you set it opaque and do \texttt{Reset A}, it
is still opaque and that may cause problems if you try to replay
tactic scripts between \texttt{A} and the current point.
\end{itemize}
\end{document}
% $Id$
|
