aboutsummaryrefslogtreecommitdiffhomepage
path: root/TODO
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 12:48:32 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 14:27:21 +0100
commitaf84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch)
treeb8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /TODO
parent9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff)
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'TODO')
-rw-r--r--TODO16
1 files changed, 8 insertions, 8 deletions
diff --git a/TODO b/TODO
index d6891e5f9..f24a37f38 100644
--- a/TODO
+++ b/TODO
@@ -25,29 +25,29 @@ Theories:
Doc:
-- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
+- 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
+- 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 (??)
+- faut-il mieux spécifier la sémantique de Simpl (??)
-- Préciser la clarification syntaxique de IntroPattern
+- 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
+- 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)
+- 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)