Я пытаюсь скомпилировать файл hw5.v в coq, который находится в папке plf основ программного обеспечения. Я хочу разрешить привязки и поэтому использую команду:
coq c -Q.PLF hw5.v
Но она не компилируется и выдает ошибку как coq c : -Q.PLF: нет такого файла или каталога. Это никогда не случалось раньше. Если я сделаю man coq c или coq c -v, это даст мне правильный вывод. Но он не работает с -Q или -R. Есть идеи, чтобы решить это? моя версия coq: 8.9.1