aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/polymorphism.v
Commit message (Expand)AuthorAge
* Restrict universe context when declaring constants in obligations.Gravatar Gaëtan Gilbert2017-11-25
* Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
* In close_proof only check univ decls with the restricted context.Gravatar Gaëtan Gilbert2017-11-24
* restrict_universe_context: do not prune named universes.Gravatar Gaëtan Gilbert2017-11-24
* Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
* test-suite: polymorphismGravatar Matthieu Sozeau2017-09-19
* Allow declaring universe binders with no constraints with @{|}Gravatar Gaëtan Gilbert2017-09-19
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Disable debug printingGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Fix bugsGravatar Amin Timany2017-06-16
* Type@{_} should not produce a flexible algebraic universe.Gravatar Gaetan Gilbert2017-05-03
* Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* Fix incompleteness of conversion used by evarconvGravatar Matthieu Sozeau2015-06-28
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Fix restrict_universe_context removing some universes that do appear in the t...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 00:58:41 +0000