ギークもどきの日記帳

雑多な知識が垂れ流される場所。ほとんど無害。

Coq 8.7.1でSoftware Foundationsを読もうとしてハマったメモ

Software FoundationsのProgramming Language FoundationsのEquiv.vをProof Generalで読み込んだら以下のようなエラーが出た。

Error:
The file /Users/yuya/dev/src/local/softwarefoundations/plf/Maps.vo contains library
Top.Maps and not library Maps

以下のような内容の_CoqProjectというファイルを作成すると上手く読み込めた。

-R "." Top

Coqの物理パスと論理パスの扱いに絡む問題っぽい。