是否可以删除/覆盖 Coq 中现有的强制转换？

Question

我导入了一个定义强制转换的 Coq 模块，但它不符合我的需要。有没有办法删除或（本地）覆盖它？

具体来说，假设我导入的模块定义了一个强制

Coercion bool_to_nat (b:bool) := match b with true => 1 | false => 0 end.

但我想在我的代码中使用相反的

Local Coercion bool_to_nat' (b:bool) := match b with true => 0 | false => 1 end.

Coq 给出警告Ambiguous paths: [bool_to_nat'] : bool >-> nat并简单地忽略我的定义（可以通过Goal false + 1 = true. reflexivity. Qed. 是否可以说服 Coq 尊重我的选择，至少在这个文件本地？

能够在声明后显式操作强制转换将是一个加分项，例如如何操作提示数据库。有这样的命令吗？

Answer 1

使用 Coq 8.15，您可以导入除强制转换之外的所有内容：

Import -(coercions) ModuleName.

比照。进口类别手册。