HoTT/HoTT — pull request #452 by JasonGross (2014-09-01 18:27:49+00:00)
Title: Remove a useless match

Discovered as useless due to a bug in Coq trunk:
https://coq.inria.fr/bugs/show_bug.cgi?id=3561