Есть ли способ отменить импорт или скрытие базовых библиотек в coq?
Вы можете избежать включения стандартной библиотеки, передав -nois в coqtop или coqc.
-nois
coqtop
coqc
Также возможно создать другое начальное состояние (которое вы можете передать в -is. В этом есть некоторый код для этого (хотя в нем нет ничего интересного).
-is