aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/Derive
Commit message (Expand)AuthorAge
* Derive plugin: add some comments.Gravatar Arnaud Spiwack2014-07-23
* Derive plugin: code reorganisation for clarity.Gravatar Arnaud Spiwack2014-07-23
* Derive plugin: small refactoring.Gravatar Arnaud Spiwack2014-07-23
* Derive plugin: a more general interface.Gravatar Arnaud Spiwack2014-07-23
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Fix derive plugin to properly treat universesGravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fix g_derive.ml4.Gravatar Arnaud Spiwack2013-12-04
* Derive plugin.Gravatar Arnaud Spiwack2013-12-04