From cb985b826fc82f94186b849206504d7d328b70e5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 10 Jan 2007 14:00:57 +0000 Subject: Nouvelle approche pour le discharge modulaire - Avant : une unique méthode discharge_function qui avait accès à l'ancien environnement mais pas de possibilité de raisonner avec les objets du nouvel environnement en cours de construction. C'était problématique pour le discharge des implicites, arguments scope, etc qui étaient finalement faits en même temps que le discharge des constantes et inductifs mais avec pour effets de bord que les entrées dans la lib_stk arrivaient juste avant celles des constantes et inductifs avec des problèmes pour effacer les bonnes entrées au moment du reset - Maintenant : deux méthodes distinctes : discharge_function qui est appliquée pour collecter de l'ancien environnement ce qui est à garder dans la section et rebuild_function qui reconstruit le nouvel environnement connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant l'extensibilité que la méthode ancienne du fichier discharge.ml ne permettait pas) Au passage, ajout d'un modificateur Global aux déclarations d'implicites et d'arguments scopes pour indiquer qu'elles doivent perdurer à la sortie de la section Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps discharged reste) Au passage, nettoyage impargs.ml, suppression code mort résiduel du traducteur etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 909de4277a..4331f3f651 100644 --- a/CHANGES +++ b/CHANGES @@ -1,4 +1,10 @@ -Changes from V8.1beta to V8.1beta2 +Changes from V8.1gamma to ... +============================= + +- Added option Global to "Implicit Arguments" and "Arguments Scope" for + section surviving + +Changes from V8.1beta to V8.1gamma ================================== Syntax -- cgit v1.2.3