aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4293.v
AgeCommit message (Expand)Author
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau