aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/namedunivs.v
Commit message (Expand)AuthorAge
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Changed syntax of explicit universes.Gravatar Matthieu Sozeau2014-06-23
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04