diff options
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) + + |