导入Coq的Bits库时如何屏蔽导入阶段的特定或全部警告

你可以通过Coq的警告控制指令实现按需屏蔽，以下是几种常见方案：

方案1：局部临时屏蔽指定警告（最推荐） #

仅在导入Bits库时关闭ambiguous-paths警告，导入完成后立即恢复，不会影响你自己代码的警告检测：

(* 临时关闭歧义强制路径警告 *)
Set Warnings "-ambiguous-paths".
From Bits Require Import bits.
(* 恢复警告，避免遗漏你自己代码中的同类问题 *)
Set Warnings "+ambiguous-paths".

方案2：全局屏蔽该类警告 #

如果你确认所有ambiguous-paths警告都来自第三方库导入，不需要关注，可以在编译层面全局配置：

• 若使用coqc直接编译，添加参数：coqc -w -ambiguous-paths 你的源文件.v
• 若使用coq_makefile，在项目根目录的_CoqProject文件中添加一行：-w -ambiguous-paths
• 若使用dune构建，在对应Coq库的dune配置中添加编译参数：

  (coq.theory
   (name your_project)
   (flags :standard -w -ambiguous-paths))
  

方案3：临时屏蔽所有导入阶段警告（不推荐） #

如果需要屏蔽导入阶段所有类型的警告，可以用以下写法，但可能会漏掉其他有价值的导入错误提示：

Set Warnings "-all".
From Bits Require Import bits.
Set Warnings "+all".

补充说明：该警告本质是Bits库为nat类型定义了多条到VWORD的强制转换路径，Coq检测到转换歧义给出的提示，不会影响代码编译的正确性，屏蔽该警告是安全的。

内容的提问来源于stack exchange，提问作者Proof-By-Sledgehammer