在看QuickChick项目的时候，遇到了一句Require Import Ltac.我不知道这是做什么的，Ltac模块在哪里。我找到了一个文件plugins/ltac/Ltac.v，但这不可能是那个文件，因为这个文件是空的（顺便说一句，包含一个空文件的目的是什么？）。我试过了，Locate Ltac.但我得到了Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable]).，这更令人困惑。
模块做什么Ltac，文件在哪里Ltac.v，为什么Loacte在这种情况下命令不起作用？谢谢！
Require Import Ltac.确实是Coq.ltac.Ltac你找到的空文件！我不确定为什么那里有一个空文件，但它是在将Ltac 移动到 plugin时引入的。如果某些 Ltac 实现被移入 Coq 而不是 OCaml 插件，它可能会充当占位符。无论如何，我认为 QuickChick 没有理由导入它，除非他们预计到 Coq 会发生一些我不知道的变化。
由于与白话命令冲突Locate Ltac（这会给您一个语法错误），您需要改为Locate Module显式使用。也是如此Print Module。
Locate Module Ltac报告Module Coq.ltac.Ltac，它告诉您您确实在看theories/ltac/Ltac.v，并Print Module Ltac显示一个空模块。但是，第二位具有误导性，因为看起来像空的模块仍然可以有符号（这里不是这种情况，仅供参考）。