From f39e92e127d551c4d9413de9c660afce5275c341 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 13 Oct 1999 12:40:33 +0000
Subject: mise a jour

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@101 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/TODO | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/TODO b/dev/TODO
index b27cac28e0..188d677b0d 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,6 +1,14 @@
 
- o Termes
-     - introduire un constructeur pour les variables existentielles
+ o Discharge
+     - conserver les constantes dans leur section de définition
+       et redéfinir des constantes déchargées à la sortie
+
+ o Variables existentielles
+     - traiter le constructeur Evar dans les fonctions de réductions
+       (parallèlement à Const)
+     - ajouter dans Environ des fonctions d'introduction et de recherche
+       des ve
+     - unifier Meta et Evar
 
  o Lib
      - écrire une fonction d'export qui supprimme les FrozenState,
-- 
cgit v1.2.3