MAJ

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

1 files changed, 21 insertions, 132 deletions

diff --git a/PROBLEMES b/PROBLEMES
index a104219283..b392d8269f 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -1,152 +1,41 @@
+----------------------------------------------------------------------
+La synthèse du ? dans l'exemple suivant se fait en V6 mais pas en V7:
+
+Inductive Prod : Type :=  Pair : Set->Set->Prod.
+Definition Pfst := [p:Prod](let (x, _) = p in x).
+Variable P : Prod->Type.
+Variable i : Set->(P (Pair nat nat)).
+Variable j : (X:Prod)(Pfst X)->(P X)->Prop.
+Variable k : nat.
+Variable l : (P (Pair nat nat)).
+Check (!j ? k (i nat)). (* Marche en V6, pas en V7 *)
+Check (!j ? k l). (* Ne marche ni en V6 !!! ni en V7 *)
+
+----------------------------------------------------------------------
 Des CASTEDCOMMAND s'affiche dans les scripts de preuves.
 
+----------------------------------------------------------------------
 Probleme d'affichage des scripts de preuve (disparition des THEN)
 Compute affiche Cbv Beta Iota
 
-
+----------------------------------------------------------------------
 Variable + Record => clash. Exemple:
-======================================================================
+
 Section S.
 Variable F:Set.
 Record R [ F:Set; x:F ] : Set := { c : x=x }.
   =>  Error: new_isevar_sign: two vars have the same name
-======================================================================
-
-Hints Resolve fait une anomalie si la constante n'existe pas
---> CORRIGÉ
-
-(* Probleme de lancement de coqtop lorsque le fichier n'est pas sauve 
-sous emacs et qu'un lien (lock ?) .#fichier a ete cree *)
-/home/cpaulin/coq/V7/bin/coqc  -q  -I . Axioms
-Anomaly: Uncaught exception Unix.Unix_error(20, "stat", "/home/cpaulin/coq/V7/theories/Num/.#Axioms.v").
-Please report.
-make: *** [Axioms.vo] Error 1
---> CORRIGÉ (message explicatif et n'échoue plus)
 
+----------------------------------------------------------------------
 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 ...
 
-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
 plus sûr 
 REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la
 syntaxe, elle est incompatible avec L_tac.
-
-CONTRIBS
----------
-BellLabs/lazyPCF : OK
-
-Bordeaux/Additions : échec sur Realizer
-Bordeaux/SearchTrees : échec sur Realizer
-Bordeaux/TREES : échec sur Realizer
-
-Bordeaux/GROUPS : OK
-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.
-
-Lannion : échec sur Realizer
-
-Lyon/AUTOMATA : OK
-Lyon/CIRCUITS : OK
-Lyon/COINDUCTIVES : OK
-
-Lyon/IEEE754 : OK
-Rocq/MUTUAL-EXCLUSION : échec sur Realizer
-
-Rocq/ALGEBRA/SETOIDS
-File "CATEGORY_THEORY/CATEGORY/ONE.v", line 83, characters 0-61
-Error: There is an unknown subterm I cannot solve
-
-Rocq/ARITH/Chinese
-File "./Zdiv.v", line 34, characters 0-944
---> Un Refine mal typé et des 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/DEMOS 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
-
-Rocq/SCHROEDER
-File "./Schroeder.v", line 351, characters 4-52
-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: Un Rewrite ou Unfold en a trop ou pas assez fait (union.v)
-
-Rocq/RATIONAL
---> Des fichiers ML à porter
-
-Lyon/AUTOMATA OK
-Lyon/CIRCUITS OK
-Lyon/COINDUCTIVES 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
-Lyon/FIRING-SQUAD : des identificateurs avec le symbole $ !! (plus autorisé)
-Lyon/INSERTION-SORT : Nécessite Programs.v
-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
-
-Montevideo/CtlTctl OK
-Montevideo/RailroadCrossing OK (TemporalOperators.v ne doit pas etre compile)
-
-Nancy/FOUnify OK
-
-Nijmegen OK
-
-Paris/ZF OK
-
-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