Я получил ту же ошибку, что и в этом вопросе: Ошибка Coqide: скомпилированная библиотека Basics.vo делает несогласованные предположения относительно библиотеки
Error:
Compiled library my_bool (in file /Users/Satan/lf_Satan/my_bool.vo) makes inconsistent assumptions over library Coq.Init.Logic
вопрос и ответ, которые я связал, объясняют, что ошибка связана с несовпадением версии Coq. Я понятия не имею, почему у меня несоответствующая версия Coq. Я пытаюсь что-то скомпилировать в терминале во время разработки в Proof General. Может ли это быть несоответствие версии?