如何在Coq内部查看库提供的所有自定义策略？

Coq里没有直接一键列出某个库所有自定义策略的命令，但可以通过以下几种方式实现需求：

• 用Search Ltac指定命名空间：自定义策略大多用Ltac关键字定义，你可以通过指定库的命名空间来筛选该库下的所有这类策略。比如要查看Coq.Lists.List库的自定义策略，执行：

  Search Ltac in Coq.Lists.List.
  

• 搜索Tactic Notation定义的策略：有些自定义策略是通过Tactic Notation语法糖定义的（比如简化版的调用接口），用下面的命令可以搜索这类策略：

  Search Tactic Notation in Coq.Lists.List.
  

• 打印指定模块的所有Ltac：如果知道库对应的模块名，可以用Print Ltac结合模块名，比如：

  Print Ltac Coq.Lists.List.
  

  这个命令会输出该模块下所有用Ltac定义的策略细节。
• 查看已加载模块的所有策略：如果已经导入了目标库（比如Require Import Coq.Lists.List.），直接执行Print Ltac.会打印当前上下文所有可见的自定义策略，其中就包含该库提供的部分。

注意：部分库可能会把策略封装在子模块里，这时候需要逐层指定子模块的命名空间来搜索。

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