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の物理パスと論理パスの扱いに絡む問題っぽい。
