Как устранить ошибку импорта суффикса coq (физический путь привязан к логическому пути)
Вероятно, это вопрос новичка, но я не смог найти готовое решение, поэтому я буду просить здесь для справки. Версия Cocq 8.5pl2
Я пытался собрать coqfj. Первый make попытка не удалась с некоторой ошибкой в строке 37 в src/FJ/ClassTable.v, Этот вопрос не об этой ошибке.
Присмотревшись, я открыл ClassTable.v в Emacs пробные и прессованные C-c C-nили альтернативно запустить coqc src/FJ/ClassTable.v, Результатом является ошибка в строке 1:
File "./src/FJ/ClassTable.v", line 1, characters 15-23:
Error: Cannot find a physical path bound to logical path matching suffix FJ.
Похоже импорт require import FJ.Lists не может быть решен (хотя FJ используется в качестве префикса, а не суффикса). Я заметил что make уже создал скомпилированный файл src/Lists.vo, который должен быть подобран coqc.
Как сказать coqc, что он должен разрешить этот "суффикс", посмотрев на *.vo или же *.v файлы в src папка?