From 323af0fd83d1d23c9b0324b19f2fa542419653ab Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 19 Apr 2017 06:18:14 +0200 Subject: Removing TODO file which is unused for more than 10 years. Hoping this is ok for everyone, otherwise we can discuss about it. --- TODO | 53 ----------------------------------------------------- 1 file changed, 53 deletions(-) delete mode 100644 TODO diff --git a/TODO b/TODO deleted file mode 100644 index f24a37f389..0000000000 --- a/TODO +++ /dev/null @@ -1,53 +0,0 @@ -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 ) - -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) - - -- cgit v1.2.3