diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:48:32 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 14:27:21 +0100 |
commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /TODO | |
parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'TODO')
-rw-r--r-- | TODO | 16 |
1 files changed, 8 insertions, 8 deletions
@@ -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) |