Search code examples
coq

How to import the file in other project/directory by configuring the Makefile or _Coqproject in current project

I would like to import the file of one of my projects when coding the current project.

i.e. Import the file ../ProjectA/fileA.v in ./fileB.v.

How can I do this via configuring the Makefile or _Coqproject.

Solution

  • You add the following line at the beginning of the _CoqProject:

    -R ../ProjectA SomeName

    And then you should be able to write

    From SomeName Require Import fileA.