HoTT/HoTT — pull request #442 by JasonGross (2014-08-28 18:39:04+00:00)
Title: Add a [transparent assert] tactic

I hope we'll one day have an OCaml version in the stdlib, because this
one has some infelicities
(https://coq.inria.fr/bugs/show_bug.cgi?id=3551). I think we need an
OCaml version to do [transparent assert (foo : nat = nat)] rather
than [transparent assert (foo : (nat = nat))], and so that we can have
both [transparent assert (foo : bar)] and just [transparent assert
(bar)]. Currently, you must name all the hypotheses that you
[transparent assert].