Coq 命令 Require Import Ltac 的作用是什么？

Question

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

Answer 1

Require Import Ltac.确实是Coq.ltac.Ltac您找到的空文件！我不确定为什么那里有一个空文件，但它是在Ltac 移动到插件时引入的。如果某些 Ltac 实现被移入 Coq 而不是 OCaml 插件，那么它可能会充当占位符。无论如何，我认为 QuickChick 没有理由导入它，除非他们预计 Coq 会发生一些我不知道的变化。

由于与白话命令冲突Locate Ltac（这会导致语法错误），因此您需要Locate Module显式使用。也同样如此Print Module。

Locate Module Ltacreports Module Coq.ltac.Ltac，它告诉您您确实正在查看theories/ltac/Ltac.v，并Print Module Ltac显示一个空模块。然而，第二位是误导性的，因为看起来像空模块的东西仍然可以有符号（这里不是这种情况，仅供参考）。