HoTT/HoTT — pull request #446 by JasonGross (2014-08-31 18:51:27+00:00)
Title: Don't match on pairs where we don't need to

It's slightly better style, I think, to do it this way. Also, when we
move to primitive projections, this code will break (see
https://coq.inria.fr/bugs/show_bug.cgi?id=3558).