From 6fcb7be2e6dfb020bd0de6626d8f386cd43e8b8b Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 25 Sep 2001 06:17:00 +0000 Subject: MAJ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2061 85f007b7-540e-0410-9357-904b9bb8a0f7 --- TODO | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/TODO b/TODO index 5a22541dd7..143e93f978 100644 --- a/TODO +++ b/TODO @@ -1,8 +1,6 @@ Distribution: - faire une passe sur les options de coqtop et coqc -- remercier les auteurs des contributions de la lib standard (p.ex. ZArith) FAIT -- changer Zarith/ en ZArith/ FAIT CP Langage: @@ -16,10 +14,8 @@ Noyau: Vernac: -- Pb noms cachés (utilisation de noms absolus ?) - Print / Print Proof en fait identiques ; Print ne devrait pas afficher les constantes opaques (devrait afficher qqchose comme ) -- Print Section imprime-t-il les sections ouvertes ou bien fermees ?? Grammaires: @@ -27,24 +23,15 @@ Grammaires: Doc: -- restriction de syntaxe pour Cbv Delta [- toto]. FAIT -- documenter tactiques NewInduction, LetTac, NewDestruct, Assert FAIT - 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 - documenter le langage de tactique et Field -- revoir le chapitre sur les tactiques utilisateur -- clarifier la sémantique de Decompose (i.e. travaille pas sous les ->) FAIT +- revoir le chapitre sur les tactiques utilisateur - faut-il mieux spécifier la sémantique de Simpl (??) -- vérifier si Print Table id est à jour - documenter @Definition and co -- rectifier le paragraphe sur Coercions et pretty-printing - + Set Printing Coercions - - Suggestions de la formation Dans le Intros pattern on pourrait interpreter les _ -- cgit v1.2.3