aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/table.mli
AgeCommit message (Expand)Author
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
2010-07-07Extraction: some more work on the (re)naming frameworkletouzey
2010-07-05Extraction: (yet another) rework of the renaming codeletouzey
2010-06-10Extraction Implicits: can accept argument names instead of just positionsletouzey
2010-06-08Extraction with implicits: perform the occur-check after optimisationsletouzey
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
2010-04-30Extraction: an experimental command to get rid of some cst/constructor argumentsletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey