diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-26 16:52:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-26 16:52:35 +0000 |
| commit | aa71bb2a686de96e792479870ef2f56fde84af09 (patch) | |
| tree | 381468db6fdc2ad56fae67f8ff5003804719f719 /PROBLEMES | |
| parent | e7140d45b65e47dc195c0c5c8f21c9251b6f3814 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1225 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 33 |
1 files changed, 24 insertions, 9 deletions
@@ -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é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) +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 |