Mise a jour Rbase

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

1 files changed, 20 insertions, 0 deletions

diff --git a/PROBLEMES b/PROBLEMES
index 11f2ecb15..c0ad725e1 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -1,3 +1,5 @@
+Hints Resolve fait une anomalie si la constante n'existe pas
+
 Declaration de Local a l'interieur d'un but ...
 Certains Clear deviennent impossible car la variable apparait dans 
 un lemme local, c'est plutot sain ...
@@ -24,8 +26,24 @@ Bordeaux/EXCEPTIONS : OK
 Dyade/Otway-Rees : OK
 Dyade/BDD : 
 File "./bdd4.v", line 122, characters 10-28
+<<<<<<< PROBLEMES
+Error: Tactic generated a subgoal identical to the original goal.
+
+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/IEEE754 : OK
 Rocq/MUTUAL-EXCLUSION : échec sur Realizer
 
 Rocq/COC
@@ -89,6 +107,8 @@ 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