From e028c3805ed0ac57d14a25cd68e567df46bff62d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Apr 2001 03:05:37 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1568 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 TODO | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/TODO b/TODO
index 78bb23b492..528319468b 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
+
+
-- 
cgit v1.2.3