diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /TODO | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'TODO')
-rw-r--r-- | TODO | 53 |
1 files changed, 53 insertions, 0 deletions
@@ -0,0 +1,53 @@ +Langage: + +Distribution: + +Environnement: + +- Porter SearchIsos + +Noyau: + +Tactic: + +- Que contradiction raisonne a isomorphisme pres de False + +Vernac: + +- Print / Print Proof en fait identiques ; Print ne devrait pas afficher + les constantes opaques (devrait afficher qqchose comme <opaque>) + +Theories: + +- Rendre transparent tous les theoremes prouvant {A}+{B} +- Faire demarrer PolyList.nth a` l'indice 0 + Renommer l'actuel nth en nth1 ?? + +Doc: + +- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection +- Documenter le filtrage sur les types inductifs avec let-ins (dont la + compatibilite V6) + +- 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 +- revoir le chapitre sur les tactiques utilisateur +- faut-il mieux spécifier la sémantique de Simpl (??) + +- Préciser la clarification syntaxique de IntroPattern +- preciser que Goal vient en dernier dans une clause pattern list et + qu'il doit apparaitre si il y a un "in" + +- Omega Time debranche mais Omega System et Omega Action remarchent ? +- Ajout "Replace in" (mais TODO) +- Syntaxe Conditional tac Rewrite marche, à documenter +- Documenter Dependent Rewrite et CutRewrite ? +- Ajouter les motifs sous-termes de ltac + +- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) +- mettre à jour la doc de induction (arguments multiples) (Pierre C.) +- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) +--> mettre à jour le CHANGES (vers la ligne 72) + + |