From 96215e28aa09d2a178166b11809e00e7f58d248f Mon Sep 17 00:00:00 2001 From: delahaye Date: Mon, 25 Dec 2000 22:32:51 +0000 Subject: 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 --- CHANGEMENTS | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) (limited to 'CHANGEMENTS') 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. -- cgit v1.2.3