如您在软件基础书籍中所见，例如在列表章节中，有一些校样被取消(在页面中搜索取消(，您可以通过按下+按钮来展开它们。我想这本书是用coqdoc制作的，所以在生成HTML文件时应该有一种方法来消除一些我找不到的证明。我想创建一个文档，我更喜欢省略一些长的证明，并想知道它是如何完成的。
您可以使用coqdocjs使校样在生成的HTML中可折叠。
Software Foundations的做法不同，它有自己的内部脚本，通过替换一些特殊的注释来调整HTML。但最终的结果是相似的。