aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareUniv.ml
AgeCommit message (Expand)Author
2020-01-21Typo in an anomaly message.Hugo Herbelin
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias