aboutsummaryrefslogtreecommitdiff
path: root/library/misctypes.ml
AgeCommit message (Expand)Author
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias