From 0f420f99550596a416fbd313ad612dec5acea8fb Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 6 Dec 2000 09:21:24 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1060 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 PROBLEMES | 9 +++++++++
 1 file changed, 9 insertions(+)

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 
-- 
cgit v1.2.3