From 6d2ba68e80cb2c21064190b9f48454cb64b231b8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Jan 2001 22:02:53 +0000
Subject: MAJ

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

(limited to 'PROBLEMES')

diff --git a/PROBLEMES b/PROBLEMES
index c1467caba3..43be1f5f40 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -1,4 +1,5 @@
 Hints Resolve fait une anomalie si la constante n'existe pas
+--> CORRIGÉ
 
 (* Probleme de lancement de coqtop lorsque le fichier n'est pas sauve 
 sous emacs et qu'un lien (lock ?) .#fichier a ete cree *)
@@ -60,7 +61,8 @@ File "./Int_typ.v", line 209, characters 30-44
 Problème d'alias dépendant dans un Cases (idem SUBST)
 
 Rocq/ALGEBRA/SETOIDS
---> Token "=_S" non reconnus
+File "CATEGORY_THEORY/CATEGORY/ONE.v", line 83, characters 0-61
+Error: There is an unknown subterm I cannot solve
 
 Rocq/ARITH/Chinese
 File "./Zdiv.v", line 34, characters 0-944
-- 
cgit v1.2.3