2021-4-8 22:57COQ开发团队致谢最近的讨论（在COQ-Club邮件列表中开始）COQ＆＃39; s徽标和名称。 我们要感谢所有参与这些讨论的人。 经历了骚扰或尴尬局面的人，关于学生（特别是女性）的人，他们最终没有学习/使用COQ，这一切都非常重要，以便社区充分认识到当前名称及其俚语的影响 英语中的意思，特别是关于COQ社区的性别......
2021-2-18 23:50Enrico Tassi在2021年1月7日提交重点：对符号处理的许多改进，包括数字符号，递归符号和带绑定的符号。 一种新算法选择了可用于打印表达式的最精确的符号，这可能会导致打印行为的变化。
2020-11-22 5:38Alectryon（以希腊小鸡之神的名字命名）是用于编写将Coq代码和散文混合在一起的技术文档的工具的集合，这种风格有时称为识字编程。
Coq证明很难孤立地理解：与纸质证明不同，证明脚本仅记录要采取的步骤（在x上进行归纳，应用定理，…），而不记录这些步骤导致的状态（目标）。结果，如果没有诸如CoqIDE或Proof......