coq/contrib/extraction/TODO, branch master

extraction: update of README+CHANGES, rm of BUGS+TODO

2009-02-27T17:04:45+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11949 85f007b7-540e-0410-9357-904b9bb8a0f7

TODO

2003-11-12T02:09:36+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4857 85f007b7-540e-0410-9357-904b9bb8a0f7

maj status de l'extraction des modules

2003-02-03T01:37:03+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3649 85f007b7-540e-0410-9357-904b9bb8a0f7

maj V7.4

2003-01-23T00:28:42+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3599 85f007b7-540e-0410-9357-904b9bb8a0f7

* empty log message *

2002-04-18T13:15:51+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2657 85f007b7-540e-0410-9357-904b9bb8a0f7

maj doc extraction dans repertoire contrib/extraction

2002-04-15T09:34:49+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2643 85f007b7-540e-0410-9357-904b9bb8a0f7

un peu de mise a jour de la doc extraction

2002-03-15T13:47:50+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2535 85f007b7-540e-0410-9357-904b9bb8a0f7

maj

2001-05-22T14:48:01+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1760 85f007b7-540e-0410-9357-904b9bb8a0f7

TODO in v.o., test/Makefile moins pire, README avec ref

2001-04-24T16:38:26+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1694 85f007b7-540e-0410-9357-904b9bb8a0f7

Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.

2001-04-23T11:41:05+00:00

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