aboutsummaryrefslogtreecommitdiff
path: root/plugins/Derive/g_derive.ml4
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
2014-05-15poly: remove unused attribute to STM nodes and vernac classificaitonEnrico Tassi
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2013-12-04Fix g_derive.ml4.Arnaud Spiwack
2013-12-04Derive plugin.Arnaud Spiwack