From 024c6aa351ad2e47ac8cb001c3fd61df3c8ebe7a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Dec 2000 22:33:32 +0000
Subject: MAJ

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

diff --git a/PROBLEMES b/PROBLEMES
index c34cfaddb3..d7d4c2fb69 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -67,11 +67,13 @@ Rocq/MUTUAL-EXCLUSION/
 Rocq/COC
 File "./Conv_Dec.v", line 68, characters 2-459
 Error: Inference of annotation not yet implemented in this case
+--> PROBLEME DISPARU 
 
 Rocq/ARITH/Chinese
 File "./Zdiv.v", line 34, characters 0-944
 Anomaly: Search error. Please report.
-Refine 
+Refine
+--> PROBLEME RESOLU MAIS LE MESSAGE D'ERREUR RESTE PAS TRES CLAIR
 
 Rocq/PARADOXES
 File "./BuraliForti.v", line 176, characters 0-26
@@ -89,6 +91,8 @@ Rocq/SCHROEDER
 File "./Functions.v", line 95, characters 0-15
 Error: Bad inductive definition.
 A la fermeture de section
+--> RESOLU Mais pb de "Remark" local à un thm pas pris en compte dans
+l'environnement de la preuve de ce théorème
 
 Rocq/SUBST
 File "./TS.v", line 69, characters 0-6
-- 
cgit v1.2.3