The Coq mailing list

["Eduardo Gimenez" <Eduardo.Gimenez AT trusted-logic.fr>]

> Coq doesn't really throw away proof terms even for opaque lemmas, does
> it? I don't see any difference in size of the .vo files at all whether
> "Save" or "Defined" is used.

When you develop a proof of T that uses the lemma L, you may either place
just the name L of the
lemma, or directly insert in T the proof of it. This latter case arrives
when you simplify your goal and
MyLemma is not an opaque constant. If you insert the proof of L, the size of
T may be considerably
increased.

Cheers,
Eduardo Gimenez.