aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Projections.v
AgeCommit message (Expand)Author
2020-04-13Simplifying the declaration of constants bound to primitive projections.Hugo Herbelin
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert