diff options
| author | herbelin | 2000-12-26 00:03:24 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-26 00:03:24 +0000 |
| commit | f38db05d1c05f75f74c4cdcca8d27eafc9882001 (patch) | |
| tree | 2e712da5835de58895b229967f42fab052628c25 /PROBLEMES | |
| parent | f40dc2a07fa9e4a600c8032ccf5d05e8ad68dba4 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 34 |
1 files changed, 28 insertions, 6 deletions
@@ -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éorème 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 |