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.
- Nouvelles contribs:
   - CtlTctl et RailroadCrossing (Carlos Daniel Luna) [Montevideo],
   - GRAPHS-BASICS (J. Duprat) [Lyon],
   - FTA (Herman Geuvers et al) [Nijmegen], 
   - Bresenham (JCF), Diff (JCF) et PAutomata (Paulin/Freund) [Orsay],
   - Functions_in_ZFC (C. Simpson), Buchberger (L. Thery), Rsa
     (L. Thery) et Stalmarck (L.Thery, P. Letouzey) [Sophia]


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