如何获取Rocq策略的完全限定名以避免命名冲突

如何查找Rocq策略的完全限定名，以及不导入Arith时调用ring的方法 #

• 查找任意标识符（包括策略、引理、常量）完全限定名的最直接方法：临时执行Require Import 对应库.让目标标识符可以被直接调用，再执行Locate 目标标识符名.命令，Rocq会直接输出该标识符所有匹配项的完整模块路径，记录对应路径后删掉临时的Import语句即可。
• Arith.ring报错的核心原因：Arith模块本身并没有直接定义ring策略，它只是在导出列表中重新导出了Ring模块的内容——Require只会递归加载所有依赖库，但只有执行Import时，模块重新导出的内容才会被加入当前作用域，Arith模块自身的命名空间下并没有绑定ring这个名字，自然无法通过Arith.ring找到。
• 仅执行Require Arith.时的正确调用方式：Require Arith.会递归加载Arith的所有依赖库，其中就包含定义ring策略的Ring模块，直接使用Ring.ring即可调用该策略，不会导入Arith中的其他定义，也就不会引发命名冲突。

附：Stack Overflow问题类型相关说明 #

• 你提出的Rocq工具使用类问题属于标准的可落地解答的技术问题，完全符合主站「问题-答案」的Q&A格式要求，不属于仅支持回复的讨论类、元类内容，问题类型选择没有错误。
• 如果后续遇到误选问题类型、自己无法修改的情况，不需要删帖重发，可以给帖子打标记选择「需要版主干预」，说明具体情况后请当值版主帮忙调整类型即可。

内容的提问来源于stack exchange，提问作者Costava