aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/Derive/g_derive.ml4
Commit message (Expand)AuthorAge
* Derive plugin: a more general interface.Gravatar Arnaud Spiwack2014-07-23
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Fix g_derive.ml4.Gravatar Arnaud Spiwack2013-12-04
* Derive plugin.Gravatar Arnaud Spiwack2013-12-04