不要在Coq中导入符号

Question

我有两个外部模块（最好不要交替使用其源代码），它们定义相同的符号。其结果是由于以下错误，我现在不再能够同时导入两个模块：

Error: Notation _ ~ _ is already defined at level 27 with arguments at level 27,
at next level while it is now required to be at level 50 with arguments at next level,
at next level.

有没有出路？我可以想象要么不从一个模块导入符号，要么仅选择性导入。但是，浏览文档并不能说明太多。

我有机会看过吗？或您会推荐什么解决方案？

Answer 1

遗憾的是，简短的答案是“ 否”。上游已经意识到了这一限制，并且在将来的某个时候（Coq 8.9？），您有望使用“解析表”来做到这一点。

但是，有一个可接受的解决方法：使用部分来限制导入的范围。想象一下，模块a b定义了一个冲突的符号，那么您可以执行以下操作：

Require a b.

Section WithNotationA.
Import a.
...
End WithNotationA.

Section WithNotationB.
Import b.
...
End WithNotationB.