aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extraction.ml
Commit message (Expand)AuthorAge
* Extraction: more factorization of common match branchesGravatar letouzey2010-07-08
* Extraction with implicits: perform the occur-check after optimisationsGravatar letouzey2010-06-08
* Extraction: fix type_expunge_from_sign broken in last commitGravatar letouzey2010-05-01
* Extraction: an experimental command to get rid of some cst/constructor argumentsGravatar letouzey2010-04-30
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Extraction: less eta in calls to global functions, better optimization phaseGravatar letouzey2010-04-16
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
* Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e...Gravatar letouzey2010-04-16
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20