aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/UnivBinders.v
AgeCommit message (Expand)Author
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
2020-11-25Add tests for #13303Gaëtan Gilbert
2020-11-25Clean UnivBinders testGaëtan Gilbert
2018-11-13Merge PR #8760: Automatically generate names for universes.Pierre-Marie Pédrot
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
2018-11-09Fix -top for univbinders output test.Gaëtan Gilbert
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-09-21Add test for univ names of polymorphic inductives in sections.Gaëtan Gilbert
2018-08-28Close #8091: print universe context for Eval when option on.Gaëtan Gilbert
2018-08-28Fix #8291: print universe names in universe context for Check.Gaëtan Gilbert
2018-03-08Fix error with univ binders on monomorphic records.Gaëtan Gilbert
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-11-25Fix #5347: unify declaration of axioms with and without bound univs.Gaëtan Gilbert
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
2017-11-25Forbid repeated names in universe binders.Gaëtan Gilbert
2017-11-25Universe binders survive sections, modules and compilation.Gaëtan Gilbert
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-11-24Fix defining non primitive projections with abstracted universes.Gaëtan Gilbert
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-04-03Instances should obey universe binders even when defined by tactics.Gaetan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:17:25 +0000