blob: 4e522a8add7c49c8813a21c8f3ac9c99687b5b67 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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.
|
