HoTT/HoTT — pull request #143 by JasonGross (2013-07-07 20:02:56+00:00)
Title: Fix a name error

Oops. I neglected to check that a last-minute change I made to
8add452dbeb0b517a36708c07e11a2166ed2d952 worked. Now it's fixed, and checked.