The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Sep 10, 2015 at 09:19:03AM +0000, Soegtrop, Michael wrote:
> In Coq 8.5 I got the impression that proof terms are not loaded unless
> really used e.g. in a Print. A Print of an imported proof results in a
> message that an opaque proof term has been loaded from a library. Also
> the background proof mechanism of CoqIDE makes the user believe that
> Coq 8.5 can handle opaque proofs.

I don't recall if it was the case in 8.4, but for sure in 8.5 (opaque) proofs
are loaded only on demand and the flag mentioned in this thread is
ignored.  I'm sure in 8.3 the flag was needed in order to get lazy
loading of proof objects (needed only by Print and some uses of Extraction).

> Finally I wonder what effect it would have to put the proofs into a
> module and then remove the proof terms by opaque signature ascription.
> In my experience this makes the proofs more opaque than Qed does, e.g.
> they are no longer accessible to Print. Would it still be required to
> load the proof terms when such an opaque module is loaded from a
> library?

I'm not very competent about modules, but in any case opaque proofs are
stored in a flat array on the side of the rest of the data.  So the
"extra opacity" a sealed module gives to you is only due to the way Print 
works.

Best,
-- 
Enrico Tassi