Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifs

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

1 files changed, 22 insertions, 6 deletions

diff --git a/CHANGEMENTS b/CHANGEMENTS
index 8f45a25a2..e3f6b85eb 100644
--- a/CHANGEMENTS
+++ b/CHANGEMENTS
@@ -26,10 +26,11 @@ Langage
 
 Extensions de syntaxe avec Grammar et Syntax
 
-- L'analyseur syntaxique considère maintenant comme token toute suite
-  de symboles (source d'incompatibilité : il faut insérer des espaces
-  entre tokens spéciaux consécutifs). Les tokens contenant non
-  constitués de caractères spéciaux sont provisoirement interdits.
+- L'analyseur lexical considère maintenant comme lexème toute suite de
+  symboles. Des exceptions ont été codées dans l'analyseur lexical pour séparer
+  des lexèmes que l'on a l'habitude de "coller" (par exemple A->~B), mais ce
+  n'est pas exhaustif et des espaces doivent être insérés dans certains cas
+  qui n'ont pas été traités (source d'incompatibilité).
 
 - L'entrée "command" dans "Grammar" et dans les piquants s'appelle
   maintenant "constr" comme dans "Syntax".
@@ -121,10 +122,20 @@ Commandes
 - Légère restriction de la syntaxe de Cbv Delta : l'option [-myconst]
   de Cbv doit immédiatement suivre Delta
 
+- Nouveau: Debug On/Off positionne/débranche le débogueur de tactiques
+  (encore très expérimental).
+
 
 Tactiques
 
-- Langage de tactique Ltac
+- Langage de tactiques Ltac: nouvelle couche de métalangage pour traiter de
+  petites automatisations. C'est essentiellement un petit noyau fonctionnel
+  muni d'opérateurs de filtrage élaborés (sur les termes, les contextes de
+  preuves et réalisant du backtracking). Pour connaître les justifications
+  d'un tel language et se procurer une documentation provisoire de Ltac, se
+  référer à l'URL suivante:
+
+      http://pauillac.inria.fr/~delahaye/
 
 - Tactique Let renommé en LetTac et utilise le let-in primitif;
   Induction renommé en OldInduction et nouveau Induction plus
@@ -148,8 +159,13 @@ Tactiques
 
 - Unfold échoue si on lui donne en argument une définition non dépliable
 
+- Tauto et Intuition ont été intégralement réécrites en utilisant le nouveau
+  langage de tactiques Ltac. Les conséquences sont un gain considérable en
+  compacité et en performances. Tauto est totalement conservatif. Intuition
+  perd légèrement en puissance mais gagne une sémantique plus claire.
+
 - AutoRewrite ne s'occupe maintenant que du but principal et c'est les
-  Hint Rewrite qui gèrent les sous-buts générés
+  Hint Rewrite qui gèrent les sous-buts générés.
 
 - Les instantiations redondantes ou incompatibles de Apply ... with ...
   sont maintenant correctement traitées.