*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1060 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/PROBLEMES b/PROBLEMES
index e345f7f63b..d29d146d98 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -33,3 +33,12 @@ Induction a.
 
 Rocq/MUTUAL-EXCLUSION/
 	Incompatibilite interpretation des arguments de Tactic Definition
+
+Rocq/COC
+File "./Conv_Dec.v", line 68, characters 2-459
+Error: Inference of annotation not yet implemented in this case
+
+Rocq/ARITH/Chinese
+File "./Zdiv.v", line 34, characters 0-944
+Anomaly: Search error. Please report.
+Refine