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!
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).