- un effort sur la doc (ocamlweb)

 - module Nametab
 - module Impargs
 - correction bug : Parameter id : t => vérification que t est bien un type


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

1 files changed, 10 insertions, 1 deletions

diff --git a/dev/TODO b/dev/TODO
index 5a6e5b70e..76cb9dd53 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,7 +1,16 @@
 
+ o Lib
+     - é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
+       pour chaque module et non pas le graphe complet
 
  o configure
      - il faut tester la version du programme correspondant à $bytecamlc