MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1364 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 29 deletions

diff --git a/PROBLEMES b/PROBLEMES
index b279ad1d3e..a081731e5f 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -26,6 +26,7 @@ Certains Clear deviennent impossible car la variable apparait dans
 un lemme local, c'est plutot sain ...
 
 La syntaxe <A>x=y est parfois refusee
+---> N'était-ce pas quand elle était précédée d'un symbole, style ~<A>x=y ??
 
 l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les
 binding je pense) d'ou des erreurs de syntaxe ...  pure_numarg est
@@ -37,9 +38,9 @@ CONTRIBS
 ---------
 BellLabs/lazyPCF : OK
 
-Bordeaux/TREES : echec sur Realizer
-Bordeaux/Additions : echec sur Realizer
-Bordeaux/SearchTrees : echec sur Realizer
+Bordeaux/Additions : échec sur Realizer
+Bordeaux/SearchTrees : échec sur Realizer
+Bordeaux/TREES : échec sur Realizer
 
 Bordeaux/GROUPS : OK
 Bordeaux/EXCEPTIONS : OK
@@ -50,28 +51,15 @@ File "./bdd4.v", line 122, characters 10-28
 <<<<<<< PROBLEMES
 Error: Tactic generated a subgoal identical to the original goal.
 
+Lannion : échec sur Realizer
+
 Lyon/AUTOMATA : OK
 Lyon/CIRCUITS : OK
-Lyon/COINDUCTIVES : 
-File "./Specified_Streams.v", line 11, characters 0-132
-Error: Illegal application (Type Error): 
-The term SStream of type (A:Set)(nat->A->Prop)->Set
-cannot be applied to the terms
- A : Set
- x : (SStream A P)
-The 2nd term has type (SStream A P) which should be coercible to
- nat->A->Prop
-
---> Out of memory après plus de 500Mo utilisés
+Lyon/COINDUCTIVES : OK
 
 Lyon/IEEE754 : OK
 Rocq/MUTUAL-EXCLUSION : échec sur Realizer
 
-Rocq/COC
-Realizer dans Conv_Dec.v, Expr.v, Infer.v, Machine.v MyList.v Names.v
-File "./Int_typ.v", line 209, characters 30-44
-Problème d'alias dépendant dans un Cases (idem SUBST)
-
 Rocq/ALGEBRA/SETOIDS
 File "CATEGORY_THEORY/CATEGORY/ONE.v", line 83, characters 0-61
 Error: There is an unknown subterm I cannot solve
@@ -80,20 +68,23 @@ Rocq/ARITH/Chinese
 File "./Zdiv.v", line 34, characters 0-944
 --> Un Refine mal typé et des Realizer
 
-Rocq/GRAPHS
-File "./cgraph.v", line 2628, characters 14-46
-Anomaly: Search error. Please report.
+Rocq/COC
+Realizer dans Conv_Dec.v, Expr.v, Infer.v, Machine.v MyList.v Names.v
+File "./Int_typ.v", line 209, characters 30-44
+Problème d'alias dépendant dans un Cases (idem SUBST)
 
-Rocq/PARADOXES OK
-Rocq/CHECKER OK
-Rocq/COMPILER OK
 Rocq/DEMOS OK
-Rocq/HIGMAN OK
+Rocq/GRAPHS OK
 Rocq/LAMBDA OK
 Rocq/SHUFFLE OK
 Rocq/THREE_GAP OK
 Rocq/ZF OK
 
+Rocq/PARADOXES OK
+Rocq/CHECKER OK
+Rocq/COMPILER OK
+Rocq/HIGMAN OK
+
 Rocq/SUBST
 File "./inversionSL.v", line 215, characters 38-39
 Problème d'alias dépendant dans un Cases
@@ -118,7 +109,11 @@ Rocq/RATIONAL
 Lyon/AUTOMATA OK
 Lyon/CIRCUITS OK
 Lyon/COINDUCTIVES OK
-Lyon/IEEE754 OK
+
+Lyon/IEEE754 (passait dans la V7.0beta !!)
+File "./IEEE754_def.v", line 427, characters 0-1194
+Error: Some clauses are redondant
+
 Lyon/PROCESSES OK
 Lyon/PROGRAMS : Nécessite Programs.v
 Lyon/STREAMS OK
@@ -129,8 +124,6 @@ File "./fifo.v", line 181, characters 0-6
 Error: Attempt to save an incomplete proof
 --> Preuve incomplète (lié à Intuition)
 
-Rocq/MM
-
 Marseille/CCS OK
 Marseille/CIRCUITS -> Realizer