Комментарии в _CoqProject

Question

Есть ли способ иметь комментарии в файле _CoqProject?

Я бы хотел скомпилировать только часть библиотеки , без полного удаления всех остальных файлов из файла _CoqProject.

Answer 1

# рассматривается как символ комментария к остальной части строки.

Я думаю, что на данный момент это не задокументировано (см. проблема # 7647 ),Но исходный код и некоторые эксперименты показывают, что он работает.