blob: 818ee0b3ff19cf153389d4eddc6d5f17ce0e43d8 (
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
55
56
57
|
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)
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.
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)
----------------------------------------------------------------------
English version of changes is available on
http:coq.inria.fr
and
ftp://ftp.inria.fr/INRIA/coq/V7.0/Changes.ps
|
