HoTT/HoTT — pull request #395 by JasonGross (2014-05-17 17:20:48+00:00)
Title: Stick an aborted definition in a comment

Coq trunk's coqc -time doesn't like it
(https://coq.inria.fr/bugs/show_bug.cgi?id=3332)

Also coqdoc-ify comments