Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 17 deletions

diff --git a/TODO b/TODO
index 5dbac9958..e53d95f8e 100644
--- a/TODO
+++ b/TODO
@@ -1,10 +1,6 @@
-Distribution:
-
-- faire une passe sur les options de coqtop et coqc
-
 Langage:
 
-- Propager les contraintes arrière dans Cases (cf example doc/Cases.tex)
+Distribution:
 
 Environnement:
 
@@ -12,35 +8,41 @@ Environnement:
 
 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 ??
-
-Grammaires:
-
-- revoir numarg/pure_numarg dans g_tactic.ml4 (regles a factoriser)
+  Renommer l'actuel nth en nth1 ??
 
 Doc:
 
 - Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
-- Documenter le nouvel Assert x:=t.
 - Documenter le filtrage sur les types inductifs avec let-ins (dont la
-  compatibility V6)
+  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 (??)
-- documenter @Definition and co
 
-- Suggestions de la formation
-  Dans le Intros pattern on pourrait interpreter les _ 
-  comme des hypotheses sur lesquelles on ferait Clear immediatement
--> FAIT, semble-t'il
+- 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
+
+