CoqIde の同じフォルダーにあるモジュールをロードできません。
coqideSoftware Foundations からソースを読み込もうとしています。 orを含む SF ソースを含むフォルダーで coqide をcoqide ./実行しています。ファイルを開いて実行すると、次のエラーが発生します。
Error: Cannot find library Poly in loadpath
この行で：
Require Export Poly.
他のすべてのrequireコマンドでも同じです。
では、SF から coqide にプログラムをどのようにロードしていますか?