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 /kernel | |
| 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 'kernel')
0 files changed, 0 insertions, 0 deletions