Removing TODO file which is unused for more than 10 years.

Hoping this is ok for everyone, otherwise we can discuss about it.

1 files changed, 0 insertions, 53 deletions

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 <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)
-
-