From aa71bb2a686de96e792479870ef2f56fde84af09 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Dec 2000 16:52:35 +0000
Subject: MAJ

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

diff --git a/PROBLEMES b/PROBLEMES
index efb5f4a838..ac590fcea5 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -14,9 +14,9 @@ CONTRIBS
 ---------
 BellLabs/lazyPCF : OK
 
-Bordeaux/TREES :
-Bordeaux/Additions :
-  echecs sur Realizer
+Bordeaux/TREES : echec sur Realizer
+Bordeaux/Additions : echec sur Realizer
+Bordeaux/SearchTrees : echec sur Realizer
 
 Bordeaux/GROUPS : OK
 Bordeaux/EXCEPTIONS : OK
@@ -64,6 +64,12 @@ Anomaly: type_of: variable h1 unbound. Please report.
 --> Pb de "Remark" local à un thm pas pris en compte dans
 l'environnement de la preuve de ce théorème
 
+Rocq/TreeAutomata
+File "./defs.v", line 309, characters 34-47
+Error: Not a recursive eliminator: some induction hypothesis is lacking
+File "./lattice_fixpoint.v", line 29, characters 44-57
+Anomaly: Search error. Please report.
+
 Rocq/RATIONAL
 --> Des fichiers ML à porter
 
@@ -76,7 +82,10 @@ Lyon/PROGRAMS : N
 Lyon/STREAMS OK
 Lyon/FIRING-SQUAD : des identificateurs avec le symbole $ !! (plus autorisé)
 Lyon/INSERTION-SORT : Nécessite Programs.v
-Lyon/DISTRIBUTED_REFERENCE_COUNTING -> Preuve incomplète (lié à Intuition)
+Lyon/DISTRIBUTED_REFERENCE_COUNTING
+File "./fifo.v", line 181, characters 0-6
+Error: Attempt to save an incomplete proof
+--> Preuve incomplète (lié à Intuition)
 
 Marseille/CCS OK
 Marseille/CIRCUITS -> Realizer
@@ -90,15 +99,21 @@ Nijmegen OK
 
 Paris/ZF OK
 
-Sophia-Antipolis/Cours-de-Coq
-File "./Partial_order_facts.v", line 123, characters 3-96
-Error: Not an inductive product
-Sophia-Antipolis/HARDWARE ??
-Sophia-Antipolis/MATHS ??
+Sophia-Antipolis/HARDWARE OK
+Sophia-Antipolis/Cours-de-Coq OK
+
+Sophia-Antipolis/MATHS/GEOMETRY
+File "./part3.v", line 78, characters 0-5
+Error: Attempt to save an incomplete proof
+--> Changement de sémantique de Intuition
+
 Sophia-Antipolis/condom ... vide 
+
 Sophia-Antipolis/param_pi
 File "./fresh.v", line 173, characters 0-20
 Error: Too few occurences
 
+Suresnes/BDD OK
+
 Utrecht/Ramsey OK
 Utrecht/ABP OK
-- 
cgit v1.2.3