aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/UnivBinders.out
AgeCommit message (Expand)Author
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-01-09Stop [Print] from saying [is (not) universe polymorphic].Gaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
2018-11-12Automatically generate names for universes.Gaëtan Gilbert
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-21Remove hash based univ level compareGaëtan Gilbert
2018-09-21Add test for univ names of polymorphic inductives in sections.Gaëtan Gilbert
2018-09-21Universe binders are Id, not Name. Never print Var.Gaëtan Gilbert
2018-09-21Best-effort hack to provide a meaningful name for anonymous bound universes.Pierre-Marie Pédrot
2018-09-21Removing calls to AUContext.instance.Pierre-Marie Pédrot
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
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
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-24When declaring constants/inductives use ContextSet if monomorphic.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-03-01 07:45:03 +0000