MAJ

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

2 files changed, 13 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index a474a84c53..08f6075576 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,7 @@
 Métathéorie
 
-- Ajout de définitions locales (Let-In)
+- Ajout de définitions locales (Let-In) avec la syntaxe [x:=u]t. Cela
+peut entrainer des comportements nouveaux pour certaines tactiques.
 
 Parsing
 
@@ -26,6 +27,12 @@ Syntaxe des constructions
   cas de clauses par défaut redondantes auquel cas la première est prise
   avec un avertissement.
 
+- Les déclarations de constantes et de variables peuvent maintenant
+être accédées par un nom long de la forme "Logic.f_equal". La
+bibliothèque standard a maintenant une racine nommée "Coq". Tout nom
+de la forme "Coq.Logic.f_equal" dénote ainsi un chemin absolu vers une
+déclaration.
+
 Syntaxe des theories
 
 - Ajout d'une syntaxe pour les reels: ``Rexpr``.
@@ -41,7 +48,7 @@ commandes)
 
 - Le parseur par défaut des actions des règles de grammaires et des
 motifs des règles d'affichage est maintenant celui associé au nom de
-la grammaire (vernac, tactic ou constr). Donc plus de piquants
+la grammaire (vernac, tactic ou constr). Donc plus de piqants
 <:vernac:<...>> etc. Pour retourner de l'ast, il faut typer
 explicitement la grammaire avec "ast" ou "List" (renommé d'ailleurs
 "ast list"), ou, si c'est dans une règle Syntax, utiliser la quotation
@@ -96,6 +103,8 @@ Tactiques
 
 - Plus de "Require Prolog" (intégré par défaut)
 
+- Unfold échoue si on lui donne en argument une définition non dépliable
+
 Outils
 
 - deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native; 
diff --git a/TODO b/TODO
index 29d138ee5d..ab06eb4777 100644
--- a/TODO
+++ b/TODO
@@ -1,6 +1,8 @@
 Distribution:
 
 - faire une passe sur les options de coqtop et coqc
+- remercier les auteurs des contributions de la lib standard (p.ex. ZArith)
+- changer Zarith/ en ZArith/
 
 Environnement:
 
@@ -15,7 +17,6 @@ Tactiques:
 
 Noyau:
 
-- Intégrer Let dans whd_* et les fonctions de tacred
 - Gérer les alias avec un let in dans les cases
 
 Vernac: