Thanks. Just commited


On Mon, Sep 2, 2013 at 10:40 PM, Jason Gross <notifications@github.com>wrote:

> In theories/HSet.v:
>
> > @@ -98,6 +98,7 @@ Defined.
> >  End AssumeFunext.
> >
> >  Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
> > +(** This one is needed in epi_surj to coerce hProp into hSet*)
>
> Documentation nit: use [epi_surj] and [hProp] and [hSet] so that coqdoc
> will make links for you.
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6114941>
> .
>