aboutsummaryrefslogtreecommitdiff
path: root/test-suite/prerequisite/bind_univs.v
AgeCommit message (Expand)Author
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-11-25Universe binders survive sections, modules and compilation.Gaƫtan Gilbert