The Coq mailing list

[Freek Wiedijk <freek AT cs.kun.nl>]

Hi Hugo,

>As far as I know, the question whether a lemma is Opaque or
>not results of a compromise between the need for efficiency
>(transparency may induces very strong time penalty on type
>checking) and convenience for reduction.

But if a lemma is defined Opaque (with "Qed" instead of
"Defined"), you can never make it Transparant again, right?
(because the proof terms is gone by that time)  That is
sometimes inconvenient.  Does Coq have a flag to keep all the
proof terms, also for Opaque stuff?  I realize that it will
make the .vo files much bigger, but if I opt for that, is it
possible?

Freek