Parsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index c76c20a3d3..a1d55209aa 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,9 +10,22 @@ Modifications depuis la V7.0
 - 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)
-- Nouvelle tactique TrueCut qui fait la coupure du calcul des séquents
+- 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
+- Nouvelle tactique Assert qui fait la coupure du calcul des séquents
   (et dans le sens attendu)
+- Inversion peut faire des Intros until avant
 - 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.
 
 Différences oubliées dans la V7.0beta :