From f9676380178d7af90d8cdf64662866c82139f116 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 24 Nov 1999 08:19:55 +0000
Subject: Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations

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

(limited to 'dev')

diff --git a/dev/TODO b/dev/TODO
index 6b35783a25..356f1e5b60 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,14 +1,9 @@
 
- o Declare
-     - declare_eliminations
-
  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)
      - unifier Meta et Evar
 
  o Lib
@@ -29,7 +24,8 @@
      - utiliser DOPL plutôt que DOPN (sauf pour Case)
      - batch mode => pas de undo, ni de reset
      - conversion : déplier la constante la plus récente
-     - un cache pour type_of_const, type_of_inductive, type_of_constructor
+     - un cache pour type_of_const, type_of_inductive, type_of_constructor,
+       lookup_mind_specif
 
  o Lexer
      à compléter
-- 
cgit v1.2.3