aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareUniv.mli
AgeCommit message (Expand)Author
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias