当我查看 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命令在这种情况下不起作用？谢谢！