aboutsummaryrefslogtreecommitdiffhomepage
path: root/TODO
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-30 17:56:55 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-30 17:56:55 +0000
commit1c703959f703b7f1e649b5adea6703d0512ab01d (patch)
tree440529e13e184988b6adc25dea1d0cda8a0b4e97 /TODO
parenta2bdd28d1bdb93664037751b9dc84bcf7d90b6b6 (diff)
Doc de Ltac, Field et AutoRewrite -> FAIT
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2087 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'TODO')
-rw-r--r--TODO2
1 files changed, 0 insertions, 2 deletions
diff --git a/TODO b/TODO
index 143e93f97..92e86c2c2 100644
--- a/TODO
+++ b/TODO
@@ -23,12 +23,10 @@ Grammaires:
Doc:
-- 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
- une passe sur le chapitre extensions de syntaxe
-- documenter le langage de tactique et Field
- revoir le chapitre sur les tactiques utilisateur
- faut-il mieux spécifier la sémantique de Simpl (??)
- documenter @Definition and co