aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/HoTT_coq_074.v
AgeCommit message (Expand)Author
2014-05-09Refresh universes for Ltac's type_of, as the term can be used anywhere,Matthieu Sozeau