Rocq

其实就是 Coq，交互式定理证明器，从 9.0 版本后改名为Rocq。

改名

从 2021 年就开始争论的话题，主要原因是 Coq 在英语里的谐音比较下流，会造成一些误解（但其实官方不说我根本没往这方面想）。新名字 Rocq 谐音 Roc，跟以前的公鸡也比较像。