MAJ

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

1 files changed, 4 insertions, 9 deletions

diff --git a/TODO b/TODO
index 92163cdce..4fe8e2f29 100644
--- a/TODO
+++ b/TODO
@@ -3,7 +3,7 @@ Distribution:
 - Faire fonctionner coqc/coqtop en non local
 - "System Error (Failure): "input_value: code mismatch" quand on
   charge en bytecode certains .vo compilés en natif (exemple typique:
-  Ring_abstract.v)
+  Ring_abstract.v) COMPRIS, EN SUSPENS
 - où va RELATIONS/WELLFOUNDED ?
 
 Environnement:
@@ -12,7 +12,7 @@ Environnement:
 - Faire fonctionner Abstract
 - Faire fonctionner Reset
 - Décider s'il faut garder Transparent/Opaque et si oui, l'implanter
-- Ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo)
+- Ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo) FAIT
 
 Tactiques
 
@@ -23,12 +23,7 @@ Noyau:
 
 - Intégrer Let dans whd_* et les fonctions de tacred
 
-Theories:
-
-- remplacer Realizer par Refine ou autre chose dans TheoryList.v
-
-Compatibilité:
-
-- Pourquoi EAuto fait-il plus dans Ring_theory ???
+Grammaires:
 
+- pb avec les extensions constr (cf Zsyntax et Cases x of `0` => ...)