aboutsummaryrefslogtreecommitdiff
path: root/plugins/Derive/derive.mli
AgeCommit message (Expand)Author
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2014-07-23Derive plugin: a more general interface.Arnaud Spiwack
2013-12-04Derive plugin.Arnaud Spiwack