diff options
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 20 |
1 files changed, 20 insertions, 0 deletions
@@ -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 |