The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I wrote an answer to this question on Stack Overflow: https://stackoverflow.com/questions/47973317/require-import-require-import.

In your particular case, the issue is the file Foo.v is implicitly in a module called Foo. Thus the fully qualified path to magic is actually Foo.Foo.magic, and after the import it’s just Foo.magic. If you want to make just magic work, you actually want to Require Foo and then Import Foo.Foo (or remove the module Foo in Foo.v).

On Sun, Apr 12, 2020 at 7:25 PM Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

Hi;

I am really confused with Require, Export, Import, etc. I tried doing a Google search but I do not find any simple explanations.

What I want to do is to have two files Foo and Bar:

Module Foo.

  Definition magic : nat := 5.

End Foo.

Now, I want to be able to access magic inside Bar:

Module Bar.

  Require Foo.
  Import Foo.
  Check Foo.magic.
  Fail Check magic. (* How do I make this work? *)

End Bar.

What am I doing wrong?