aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/univpoly.txt
Commit message (Expand)AuthorAge
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Minor typo in universe polymorphism doc.Gravatar Maxime Dénès2015-10-09
* Univs: More info for developers.Gravatar Matthieu Sozeau2015-10-02
* Change Ltac constr matching semantics to consider universes when merging twoGravatar Matthieu Sozeau2014-06-15
* Add incompatibilities paragraph in doc about universe polymorphism.Gravatar Matthieu Sozeau2014-05-06
* Add doc on the new API for universe polymorphism and primitive projectionsGravatar Matthieu Sozeau2014-05-06