1 files changed, 34 insertions, 0 deletions
diff --git a/doc/Anomalies.tex b/doc/Anomalies.tex
new file mode 100755
index 000000000..8e23fa602
--- /dev/null
+++ b/doc/Anomalies.tex
@@ -0,0 +1,34 @@
+\documentclass[11pt]{article}
+
+\input{./title}
+
+\title{Known bugs of {\sf 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$