HoTT/HoTT — pull request #130 by SkySkimmer (2013-06-03 12:09:15+00:00)
Title: minor debug

Small error in a tactic