5

When I am looking at the QuickChick project, I encountered the sentence Require Import Ltac. I don't know what this does and where the Ltac module is. I found a file plugins/ltac/Ltac.v, but this couldn't be the one since this file is empty (by the way, what is the purpose of including an empty file anyway?). I tried Locate Ltac. but I got Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable])., which is more confusing.

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

Jian Wang
  • 103
  • 5

1 Answers1

5

Require Import Ltac. is indeed Coq.ltac.Ltac, the empty file you found! I am not sure why there's an empty file there, but it was introduced when Ltac was moved to a plugin. Perhaps it serves as a placeholder for if some of the Ltac implementation were moved into Coq rather than being an OCaml plugin. In any case I think there's little reason for QuickChick to import it, unless they're anticipating some change to Coq I don't know about.

Because of a conflict with the vernacular command Locate Ltac (which is giving you a syntax error), you need to instead use Locate Module explicitly. The same goes for Print Module.

Locate Module Ltac reports Module Coq.ltac.Ltac, which tells you that you're indeed looking at theories/ltac/Ltac.v, and Print Module Ltac shows an empty module. However, that second bit is misleading, since what look like empty modules can still have notations (that's not the case here, but just FYI).

Tej Chajed
  • 3,749
  • 14
  • 18
  • Thanks! However, I still don't know why `Locate Ltac.` fails. `Locate` works fine for almost any imported Modules. For example, if in `coqtop` you try `Require Import Morphisms.` and then `Locate Morphisms.`, it tells you `Module Coq.Classes.Morphisms` (you get the same thing if you try `Locate Module Morphisms.`). Why must I use `Locate Module` in the `Ltac` case? – Jian Wang Mar 30 '18 at 21:20
  • 2
    The reason to add this file was due to the way the build system works, IIRC. – ejgallego Mar 30 '18 at 23:51
  • 1
    @JimYu This is because `Locate Ltac` also exists, and there is a confusion between your module named `Ltac` and the `Locate Ltac` command (e.g. `Locate Ltac idtac.`). – eponier Apr 03 '18 at 11:59
  • Ah, thanks @eponier! I'll update my answer since yours is really the correct explanation. – Tej Chajed Apr 03 '18 at 16:15