Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Mutually Dependent Modules

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Mutually Dependent Modules


Chronological Thread 
  • 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.

Top of Page