aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/UnivBinders.out
AgeCommit message (Expand)Author
2021-01-13Make sure "Print Module" write a dot at the end of inductive definitions.Guillaume Melquiond
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
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-08-28In "About", print all arguments, even if it is trailing list of _.Hugo Herbelin
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-02-19ComInductive: use lbound=Prop iff non polymorphicGaëtan Gilbert
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-04Allow SProp default onGaëtan Gilbert
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
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-01-31 11:16:55 +0000