在导入时抑制警告
Suppress Warning At Import
我有一个使用 Bits 库的 Coq 项目。在代码的某些地方我有
From Bits Require Import bits.
那时我总是收到多个形式的警告
Warning:
New coercion path [natAsDWORD; DWORDtoVWORD] : nat >-> VWORD is ambiguous with existing
[natAsQWORD; QWORDtoVWORD] : nat >-> VWORD. [ambiguous-paths,typechecker]
现在，我的编译日志总是充满了我真的不关心的警告，我也看不到我的代码是否产生了任何重要的警告。
那么，如何在导入时抑制所有警告，或者至少抑制这些警告？
为此，您可以使用 Set Warnings 命令来消除警告。
Set Warnings "-ambiguous-paths".
From Bits Require Import bits.
Set Warnings "ambiguous-paths".
ambiguous-paths 在警告消息中。
我先告诉它去掉它前面有一个减号，然后我再恢复它，因为命令是全局的。
Warnings 标志是 documented here。
我有一个使用 Bits 库的 Coq 项目。在代码的某些地方我有
From Bits Require Import bits.
那时我总是收到多个形式的警告
Warning: New coercion path [natAsDWORD; DWORDtoVWORD] : nat >-> VWORD is ambiguous with existing [natAsQWORD; QWORDtoVWORD] : nat >-> VWORD. [ambiguous-paths,typechecker]
现在，我的编译日志总是充满了我真的不关心的警告，我也看不到我的代码是否产生了任何重要的警告。 那么，如何在导入时抑制所有警告，或者至少抑制这些警告？
为此，您可以使用 Set Warnings 命令来消除警告。
Set Warnings "-ambiguous-paths".
From Bits Require Import bits.
Set Warnings "ambiguous-paths".
ambiguous-paths 在警告消息中。
我先告诉它去掉它前面有一个减号，然后我再恢复它，因为命令是全局的。
Warnings 标志是 documented here。