coq - 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 was moved to a 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显示一个空模块。但是，第二位具有误导性，因为看起来像空的模块仍然可以有符号(这里不是这种情况，仅供引用)。