Как импортировать файл в другой проект / каталог, настроив Makefile или _Coqproject в текущем проекте

Question

Я хотел бы импортировать файл одного из моих проектов при кодировании текущего проекта.

т.е. импортировать файл .. / ProjectA / fileA.v в . / FileB.v .

Как я могу сделать это через настройку Makefile или _Coqproject.

Answer 1

Вы добавляете следующую строку в начале _CoqProject:

-R ../ProjectA SomeName

И тогда вы сможете написать

From SomeName Require Import fileA.