From 3586c044d9f9e48f0043bb3af1bd3fbcc78485a0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 24 Apr 2001 16:38:26 +0000
Subject: 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
---
 contrib/extraction/README        |  8 ++++++++
 contrib/extraction/TODO          | 14 ++++++--------
 contrib/extraction/test/Makefile |  2 +-
 3 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/contrib/extraction/README b/contrib/extraction/README
index bcd278b335..2a7bc05645 100644
--- a/contrib/extraction/README
+++ b/contrib/extraction/README
@@ -25,6 +25,7 @@ Translation between Coq and ML is based upon the following principles:
 
 - Terms of sort Prop don't have any computational meaning, so they are
 merged in one ML term "prop", which is for the moment the ML constant ().
+This part is done according to P. Letouzey's work (*).
 
 - Terms that are arities (i.e. something of shape ( : )( : )...s with 
 s a sort ) don't have any ML counterpart, since they are types of 
@@ -101,6 +102,13 @@ Go there.
 "make reals" to extract & compile a realization of the Reals axioms
 
 
+(*):
+Exécution de termes de preuves: une nouvelle méthode d'extraction 
+pour le Calcul des Constructions Inductives, Pierre Letouzey,
+master thesis, 2000, 
+http://www.eleves.ens.fr/home/letouzey/download/rapport_dea.ps.gz
+
+
 
 
 Any feedback is welcome: 
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 27069ffdce..1a6c406804 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.
 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 89f13c75bd..957cddcf2e 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -31,7 +31,7 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML))
 #	General rules 
 #
 
-all: $(ML) .depend $(CMO) v2ml
+all: $(ML) depend $(CMO) v2ml
 
 depend: $(ML)
 	rm -f .depend; ocamldep $(INCL) $(ML) > .depend
-- 
cgit v1.2.3