From dcfeca5f828bc2648b567616e3dfabd03e13d9ab Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 22 Nov 2000 15:09:17 +0000 Subject: deplacement poly_args; iterateurs sur les segments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7 --- TODO | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'TODO') diff --git a/TODO b/TODO index 5620502da..181748677 100644 --- a/TODO +++ b/TODO @@ -1,19 +1,14 @@ Distribution: -- Faire fonctionner coqc/coqtop en non local FAIT -- "System Error (Failure): "input_value: code mismatch" quand on - charge en bytecode certains .vo compilés en natif (exemple typique: - Ring_abstract.v) COMPRIS, FAIT -- où va RELATIONS/WELLFOUNDED ? +- faire une passe sur les options de coqtop et coqc +- option -byte à coqtop +- coqc utilise coqtop.opt par défaut, sauf si -byte indiqué Environnement: - Faire fonctionner Search - Porter SearchIsos -- Faire fonctionner Abstract FAIT -- Faire fonctionner Reset FAIT -- Décider s'il faut garder Transparent/Opaque et si oui, l'implanter FAIT -- Ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo) FAIT +- Require synchronisé Tactiques: @@ -23,6 +18,12 @@ Tactiques: Noyau: - Intégrer Let dans whd_* et les fonctions de tacred +- Gérer les alias avec un let in dans les cases + +Vernac: + +- Imprimer les paths avec "." +- Pb noms cachés (utilisation de noms absolus ?) Grammaires: -- cgit v1.2.3