coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MHonArc 2.6.18.