假设我有几个基于数据结构(或引理)的证明A。然后，我将 A 重构为 A'，是否有通用实践/工具工具让 Coq 知道所有证明都受到我的重构的影响？
感谢您对此事提供一些线索。
edit1:感谢您的所有建议，我会尝试一下，然后再回复。
最佳答案
另一个可能有用的工具是 dpdgraph ，这使得可以显示各种对象之间的所有使用依赖关系。
关于Coq 影响分析，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/50484086/