CHANGES


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