Как видно из Книги по основам программного обеспечения , например, в главе Списки есть некоторые доказательства, которые исключены (поиск исключен на странице), и вы можете расширить их, нажав кнопка +. Я предполагаю, что эта книга написана с использованием coqdoc, поэтому при создании файла HTML должен быть способ исключить некоторые доказательства, которые я не могу найти. Я хочу создать документацию, в которой я предпочитаю исключить некоторые длинные доказательства и хотел бы знать, как это делается.