The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Can someone explain to me the differences between [Lemma foo : fooT. ... Qed.] and [Lemma foo : fooT. ... Defined. Global Opaque foo.]?  The ones I know are:

The former is affected by "-dont-load-proofs", the latter is not.

The latter can later be made [Transparent], the former cannot.

Neither of these explains to me why using Qed in one place allows one of my files to compile in about 4 minutes (about 3 minutes, 45 seconds with -dont-load-proofs), but using Defined + Global Opaque in that place causes the other file to take about 90 minutes to compile.  My current hypothesis is that it has something to do with universe polymorphism, as this is using HoTT/coq.

-Jason