coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Mutually Dependent Modules

From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Mutually Dependent Modules
Date: Fri, 20 Feb 2015 10:49:22 +0000
Accept-language: en-GB, en-US
Authentication-results: spf=none (sender IP is ) smtp.mailfrom=jeffrey.terrell AT kcl.ac.uk;

Hi,

If a file contains

Require Import B.

Module A.

Variable X : nat.

<...>

End A.

is it possible to access X from module B, or any module that B happens to require?

If, as I suspect, the answer is no, what’s the recommended way of handling this situation? To place X in a separate module, and for modules A and B to require it?

Thanks.

Regards,
Jeff.

[Coq-Club] Mutually Dependent Modules, Terrell, Jeffrey, 02/20/2015