ensembles de contraintes d'univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 10 deletions

diff --git a/dev/TODO b/dev/TODO
index 76cb9dd53..ca3b7c992 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
+