aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/extraction.ml
AgeCommit message (Expand)Author
2010-04-16Util: remove list_split_at which is a clone of list_chopletouzey
2010-04-16Extraction: ad-hoc identifier type with annotations for reductionsletouzey
2010-04-16Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e...letouzey
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey