From f38db05d1c05f75f74c4cdcca8d27eafc9882001 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Dec 2000 00:03:24 +0000
Subject: MAJ

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

diff --git a/PROBLEMES b/PROBLEMES
index 5cdbfbfc24..8a245a596f 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -26,11 +26,6 @@ Dyade/BDD :
 File "./bdd4.v", line 122, characters 10-28
 --> Out of memory après plus de 500Mo utilisés
 
-Lyon/AUTOMATA : OK
-Lyon/CIRCUITS : OK
-Lyon/COINDUCTIVES : OK
-Lyon/IEEE754 : OK
-
 Rocq/MUTUAL-EXCLUSION : échec sur Realizer
 
 Rocq/COC
@@ -72,11 +67,38 @@ l'environnement de la preuve de ce th
 Rocq/RATIONAL
 --> Des fichiers ML à porter
 
-Rocq/MM
+Lyon/AUTOMATA OK
+Lyon/CIRCUITS OK
+Lyon/COINDUCTIVES OK
+Lyon/IEEE754 OK
+Lyon/PROCESSES OK
+Lyon/PROGRAMS : Nécessite Programs.v
+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)
+
+Marseille/CCS OK
+Marseille/CIRCUITS -> Realizer
 
 Montevideo/CtlTctl OK
 Montevideo/RailroadCrossing OK (TemporalOperators.v ne doit pas etre compile)
 
+Nancy/FOUnify OK
+
 Nijmegen OK
+
+Paris/ZF OK
+
+Sophia-Antipolis/Cours-de-Coq
+File "./ps.v", line 206, characters 3-31
+Error: A is already used
+Sophia-Antipolis/HARDWARE ??
+Sophia-Antipolis/MATHS ??
+Sophia-Antipolis/condom ... vide 
+Sophia-Antipolis/param_pi
+File "./fresh.v", line 173, characters 0-20
+Error: Too few occurences
+
 Utrecht/Ramsey OK
 Utrecht/ABP OK
-- 
cgit v1.2.3