aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/TODO
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-24 16:38:26 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-24 16:38:26 +0000
commit3586c044d9f9e48f0043bb3af1bd3fbcc78485a0 (patch)
tree73967eb1a0efb3fc19168ea098c38aea500c3e65 /contrib/extraction/TODO
parente7d2a1a7e87e827773051b7cce904cb1b00fe609 (diff)
TODO in v.o., test/Makefile moins pire, README avec ref
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1694 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/TODO')
-rw-r--r--contrib/extraction/TODO14
1 files changed, 6 insertions, 8 deletions
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 27069ffdc..1a6c40680 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -1,15 +1,13 @@
- 4. Cofix : seulement en Haskell
+ 5. Haskell Syntax
- 5. Syntaxe Haskell
+ 7. Eta expansion for resolving message: "variables cannot be generalized"
- 7. Eta expansion pour contourner typage Caml
+ 9. Doc!! (examples)
- 9. Doc!! (exemples)
+ 10. Comments in extraction.ml
- 10. Recommenter extraction.ml
-
- 11. tester contribs
+ 11. test contribs
- 12. garantir typage Caml => magic + cast.
+ 12. Ocaml typing => magic + cast.