From 9084393008d9cd2a1f36391e06f6a73cbc529a16 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Sat, 25 Sep 1999 14:33:49 +0000
Subject: ensembles de contraintes d'univers

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

(limited to 'dev')

diff --git a/dev/TODO b/dev/TODO
index 76cb9dd53c..ca3b7c992b 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -3,14 +3,7 @@
      - écrire une fonction d'export qui supprimme les FrozenState,
        vérifie qu'il n'y a pas de section ouvert, et présente les
        déclarations dans l'ordre chronologique (y compris dans les
-       sections fermées). A utiliser dans Library pour sauver un module.
-
- o Convertibilité
-     - utiliser une exception plutôt qu'un type somme Convert. | Non Convert.
-
- o Univers
-     - définir un type d'ensemble de contraintes, et sauver cet ensemble
-       pour chaque module et non pas le graphe complet
+       sections fermées ?). A utiliser dans Library pour sauver un module.
 
  o configure
      - il faut tester la version du programme correspondant à $bytecamlc
@@ -29,6 +22,6 @@
      à compléter
 
  o Toplevel
-     - boucle principale, affichage des erreur, du prompt
-     - parsing de la ligne de commande (utiliser Arg)
+     - parsing de la ligne de commande : utiliser Arg
+
 
-- 
cgit v1.2.3