MAJ

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

1 files changed, 4 insertions, 1 deletions

diff --git a/TODO b/TODO
index 78bb23b49..528319468 100644
--- a/TODO
+++ b/TODO
@@ -26,11 +26,12 @@ Grammaires:
 
 Doc:
 
-- restriction de syntaxe pour Cbv Delta [- toto].
+- restriction de syntaxe pour Cbv Delta [- toto]. FAIT
 - documenter tactiques Induction, LetTac
 - documenter AutoRewrite
 - Ajouter let dans les règles du CIC
   -> FAIT, mais reste a documenter le let dans les inductifs
+  et les champs manifestes dans les Record   
 - changement syntaxe de AddPath
 - une passe sur le chapitre extensions de syntaxe
 - une passe sur le chapitre Cases
@@ -42,3 +43,5 @@ Doc:
 - documenter @Definition and co
 - rectifier le paragraphe sur Coercions et pretty-printing
   + Set Printing Coercions
+
+