aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_047.v
Commit message (Expand)AuthorAge
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Add regression tests for univ. poly. and prim projGravatar Jason Gross2014-05-06