aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/polymorphism.v
AgeCommit message (Expand)Author
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
2017-11-24In close_proof only check univ decls with the restricted context.Gaëtan Gilbert
2017-11-24restrict_universe_context: do not prune named universes.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-09-19test-suite: polymorphismMatthieu Sozeau
2017-09-19Allow declaring universe binders with no constraints with @{|}Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-06-16Disable debug printingAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-05-03Type@{_} should not produce a flexible algebraic universe.Gaetan Gilbert
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-07-07Univs: bug fix.Matthieu Sozeau
2015-06-28Fix incompleteness of conversion used by evarconvMatthieu Sozeau
2014-06-04- Force every universe level to be >= Prop, so one cannot "go under" it anymore.Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-06Fix restrict_universe_context removing some universes that do appear in the t...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2006-10-30Débranchement du polymorphisme de sorte sur les définitions dans Typeherbelin
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:29:36 +0000