diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-26 14:25:52 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-26 14:25:52 +0000 |
commit | 32bdedb61aa6e574f1d8af3b729607a2bb81fa96 (patch) | |
tree | 958b6816ded631126547db428343f83b43589339 /TODO | |
parent | 317af3e75771d5fdcb5fb8d35d2aa5bd196c432f (diff) |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@771 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'TODO')
-rw-r--r-- | TODO | 15 |
1 files changed, 11 insertions, 4 deletions
@@ -1,18 +1,19 @@ 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) +- où va RELATIONS/WELLFOUNDED ? Environnement: - Faire fonctionner Search - Faire fonctionner Abstract - Faire fonctionner Reset -- Faire fonctionner Transparent/Opaque +- 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) -- Que les Infix soit chargés lors d'un Require (DONE) -- Problème de compatibilité du mode implicite au discharge (DONE) - Tactiques - Choisir la précédence de Try/Orelse @@ -25,3 +26,9 @@ Noyau: Theories: - remplacer Realizer par Refine ou autre chose dans TheoryList.v + +Compatibilité: + +- Pourquoi EAuto fait-il plus dans Ring_theory ??? + + |