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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
Modifications depuis la V7.0
- Fonctions de r�duction dans les d�finitions locales s'appliquent par
d�faut au corps de la d�finition. Extension de la notion de Clause
pour forcer l'action sur le type des d�fs seulement sous la forme
"Change c in Type of H."
- Prise en compte des qualid dans Decompose, flags de Delta, ...
- Corrections de plusieurs bugs de Coercions
- Correction bug inf�rence type Cases en pr�sence de K-r�dex
- Correction bugs Cases en cas de pr�dicat d�pendant
- Le flag Delta n'inclut plus Zeta et Evar, nouveaux flags Zeta et Evar inclus
dans Compute (� documenter)
- Prise en compte des noms longs dans Require et Import, et gestion de
modules de m�me noms situ�s dans des r�pertoires diff�rents
- Nouvelle strat�gie de r�f�renciation par nom court bas�e sur le nom de
base et plus sur les noms de module (avant un module pouvait en
cacher un autre, maintenant seul un nom de base peut en cacher un
autre -- c'est le mode de PATH sous unix)
- Plus de typage dans les quotations (les macros $LIST, ... doivent
�tre suivies d'une m�tavariable, idem pour { })
- D�veloppeur: les var des ast sont maintenant des identifiers
- Les identificateurs ne sont plus mutables
- Inversion, Injection, Discriminate, ... font des intros until
- Decompose supprime les hypoth�ses temporaires
- Nouvelle tactique Assert qui fait la coupure du calcul des s�quents
(et dans le sens attendu)
- Am�lioration de l'efficacit� de l'ancien Cut
- En cas de Require en milieu de section, les noms courts importes par
le module disparaissent a la fermeture de la section,
et les Require ult�rieurs ne les r�introduisent pas.
- NewInduction et NewDestruct sont maintenant achev�s: elles unifient
Elim et Induction, et Case et Destruct en proposant un comportement plus
"naturel" (par rapport au Induction de la V6 qui s'applique sur les
hypoth�ses du contexte, la strat�gie de nommage est
diff�rente). Elim et Case restent n�cessaires pour les cas o�
l'hypoth�se d'�limination est un produit sur un type inductif.
Diff�rences oubli�es dans la V7.0beta :
- les objets non persistants (Grammaires, Hints) d'un module charg� par Require
disparaissent � la fermeture de la section si le Require est dans la
section. Les Require ult�rieurs ne les r�introduisent pas.
- Un lieur multiple comme (a:A)(a,b,c:(P a))(Q a), n'est plus compris comme
(a:A)(a0:(P a))(b:(P a),c:(P a))(Q a0), mais comme
(a:A)(a0:(P a))(b:(P a0),c:(P a0))(Q a0)
- Les noms de variables des projections de Record sont maintenant bas�s sur
l'initiale de leur type.
Diff�rences V7.0beta / V7.0
- Portage de Correctness
- R��criture de Extraction
- Ajout de d�clarations locales aux Record (record � la Randy).
- Correction de bugs
- Identity Coercion
- Rel not in scope of ?
- implicits in inductive defs
- localisation des erreurs avec Syntactif Definition
- clauses par d�faut de Cases non lues s�quentiellement et
d�tection des cas non utilis�s
- plusieurs bugs avec les pr�dicats de Cases lorsque d�pendants
- Prise en compte noms longs dans Hints, Coercions et Unfold
- R�tablissement des @Definition and co
- R�tablissement des token extensibles et m�langeant symboles et lettres
- Ajout d'une option Set/Unset/Test Printing Coercions
- Possibilit� de d�plier des d�finitions locales � un but
- Suppression message .coqrc
- Add ML Path est fait automatiquement par Add LoadPath
- Nouveau m�canisme de nommage des sch�mas d'�limination (incompatibilit�s...)
Diff�rences oubli�es dans la V7.0beta :
- Du fait des noms qualifi�s, les variables de buts n'�vitent plus les
globaux de m�me nom de base
- Unfold ne peut s'appliquer qu'� des constantes d�pliables (en
particulier pas � des Syntactic Definition, ni des types inductifs)
----------------------------------------------------------------------
English version of changes is available on
http:coq.inria.fr
and
ftp://ftp.inria.fr/INRIA/coq/V7.0/Changes.ps
|
