aboutsummaryrefslogtreecommitdiff
path: root/engine/univSubst.ml
AgeCommit message (Expand)Author
2018-07-03Remove unused output of Universes.normalize_univ_variablesGaëtan Gilbert
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert