The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

[To: 
coq-club AT pauillac.inria.fr]

On Fri, 20 Dec 2002, Hugo Herbelin wrote:

>   Nothing is currently done not to load the opaque proofs into
> memory.

Are all the dependant modules also loaded into memory?  If B requires A, C
requires B, and D requires C, when I compile D will all of C B and A be
loaded into memory?

- -- 
Russell O'Connor            <http://www.math.berkeley.edu/~roconnor/>
``[Law enforcement officials] suggested that the activists were stopped
not because their names are on the list, but because their names resemble
those of suspected criminals or terrorists.'' -- SFGate.com
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.1 (SunOS)

iQCVAwUBPgN83k0+aO5oRkNZAQILEAP+K0ZoeSG1LdREVW8ou5yOm8gNCY6TWCwa
1/+QeT2VK/C6iNRXTD5QyvyKx3U1c3n2UuPldAY5mhQgQSyC3tjr2DKuTWBjsE/q
QUYg+9t3AAEgfeFwkg3nQdO+XrQo3NA9vCO3FIWIjOIXg2BD7IPqrTHS1UHVsiCR
lYJJ8G0+bu4=
=sOmJ
-----END PGP SIGNATURE-----