ソフトウェア基盤の plf フォルダーにある coq でファイル hw5.v をコンパイルしようとしています。バインディングを解決したいので、次のコマンドを使用します。
coqc -Q.PLF hw5.v
しかし、それはコンパイルされず、エラーとして coqc: -Q.PLF: no such file or directory が表示されます。これは今までにないことです。man coqc または coqc -v を実行すると、正しい出力が得られます。ただし、-Q または -R では機能しません。これを解決するアイデアはありますか？私のコックのバージョンは: 8.9.1