diff options
| author | letouzey | 2001-04-23 11:41:05 +0000 |
|---|---|---|
| committer | letouzey | 2001-04-23 11:41:05 +0000 |
| commit | 74e0f575f6b7efe9a457fcf621b49df8bb88d2d7 (patch) | |
| tree | ce871230ec307cbeae7459104288f01f8cd2c476 /contrib/extraction/BUGS | |
| parent | 6a05d25e60d645f6af4ed7f89f6bd22bcf129c9f (diff) | |
Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.
Du coup MLcons avec 2 args seulement.
Ne reclame pas de realiser axioms sur Prop.
Optimizations=true par default pour Extraction Module.
Simplifications naives des letin.
Merge_app avant normalisation.
Booleen expansion_test pour l'optimisation, avec test de strictness.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1662 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/BUGS')
| -rw-r--r-- | contrib/extraction/BUGS | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/extraction/BUGS b/contrib/extraction/BUGS index 8b13789179..7f3f59c190 100644 --- a/contrib/extraction/BUGS +++ b/contrib/extraction/BUGS @@ -1 +1,2 @@ - +It's not a bug, it's a lack of feature !! +Cf TODO. |