blob: 3b2dcacd4db4123645a3d0a9fadbe105018e99bc (
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
|
Diff�rences V7.0beta / V7.0
- Ajout de d�clarations locales aux Record (record � la Randy).
- Correction de bugs (Identity Coercion; Rel not in scope of ?;
implicits in inductive defs).
- 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
- Possibilit� de d�plier des d�finitions locales � un but
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
----------------------------------------------------------------------
English version of changes is available on
http:coq.inria.fr
and
ftp://ftp.inria.fr/INRIA/coq/V7.0/Changes.ps
|
