diff options
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 54 |
1 files changed, 0 insertions, 54 deletions
diff --git a/PROBLEMES b/PROBLEMES deleted file mode 100644 index 4e522a8a..00000000 --- a/PROBLEMES +++ /dev/null @@ -1,54 +0,0 @@ -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. |