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