aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/polymorphism.v
Commit message (Expand)AuthorAge
* 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 12:27:03 +0000