diff options
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/PROBLEMES b/PROBLEMES new file mode 100644 index 00000000..4e522a8a --- /dev/null +++ b/PROBLEMES @@ -0,0 +1,54 @@ +Intuition plante en 7.1 à certains endroits où il réussissait en 6.3. +Y a-t-il une explication ? (cf contrib sheaves de Chicli - HH) + +---------------------------------------------------------------------- +Theorem toto : (A:Prop)A->A. +Refine [A;x]?. +produit le message "type_of: this is not a well-typed term. Please report." + +---------------------------------------------------------------------- +"Intro until 1" plante avec le message +"Error: Internal tactic intro cannot be applied to intro until #GENTERM 1" +--> intro est répété + GENTERM + +---------------------------------------------------------------------- +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 + +---------------------------------------------------------------------- +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 ... + +---------------------------------------------------------------------- +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. |