aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/univGen.ml
Commit message (Collapse)AuthorAge
* Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
| | | | (Universes and Evd)
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17