What does the Coq Require Import Ltac team do?

Question

When I look at the QuickChick project, I came across the Require Import Ltac. I do not know what this does and where the Ltac module is Ltac . I found the plugins/ltac/Ltac.v , but this could not be so, since this file is empty (by the way, what is the point of including an empty file?). I tried Locate Ltac. but I got Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable]). that is more confusing.

What does the Ltac module Ltac , where is the Ltac.v file, and why does the Loacte command work in this case? Thanks!

Answer 1

Require Import Ltac. really Coq.ltac.Ltac , the empty file you found! I'm not sure why there is an empty file there, but it was introduced when Ltac was moved to the plugin . Perhaps it serves as a placeholder so that part of the Ltac implementation is moved to Coq, rather than the OCaml plugin. In any case, I think that there is a small reason for QuickChick to import it, if they do not foresee some changes in Coq, which I do not know about.

Due to a conflict with the Locate Ltac user command (which gives you a syntax error), you must explicitly use the Locate Module instead. The same goes for the Print Module .

Locate Module Ltac tells Module Coq.ltac.Ltac , which says you are really looking at theories/ltac/Ltac.v , and Print Module Ltac shows an empty module. However, this second bit is misleading, because what looks like empty modules can still be labeled (this is not, but only FYI).