diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 15:09:17 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 15:09:17 +0000 |
commit | dcfeca5f828bc2648b567616e3dfabd03e13d9ab (patch) | |
tree | e6ff8cddaa26116cd023bc30e790aa6aa2da0f61 /TODO | |
parent | 24cb368c8cda29daa0c34a807e49146c4885226a (diff) |
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
Diffstat (limited to 'TODO')
-rw-r--r-- | TODO | 19 |
1 files changed, 10 insertions, 9 deletions
@@ -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: |