PROBLEMES


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.