aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/universes.ml
Commit message (Expand)AuthorAge
...
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06