import - 不要在 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

不幸的是，简短的回答是 没有 . Upstream 意识到了这个限制，并且在 future 的某个时候(Coq 8.9？)，您希望能够使用“解析表”来做到这一点。

但是，有一个可接受的解决方法:使用部分来限制导入的范围。想象模块a b定义一个冲突的符号，那么你可以这样做:

Require a b.

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

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