CODEWITHSUNDEEP
coq
Khan
Khan

Reputation: 303

Locating definition of a tactic in Coq proofs

In studying Coq proofs of other authors, I often encounter a tactic, lets say "inv eq Heq" or "intro_b". I want to understand such tactics.

How can I find if it is a Coq tactic or a Tactic Notation defined somewhere in my current project?

Second, is there a way to find its definition?

I used SearchAbout, Search, Locate and Print but could not find answers to the above questions.

Upvotes: 6

Views: 593

Answers (2)

Clément
Clément

Reputation: 12917

As mentioned before, Print Ltac ... prints the code of a user-defined tactic.

To locate a user-defined tactic (i.e. to know where its defined), use Locate Ltac .... It gives you the fully qualified name. Then use Locate Library to find the corresponding file.

Upvotes: 2

Ptival
Ptival

Reputation: 9437

You should be able to use

Print Ltac <tacticname>.

to print the code of a user-defined tactic (according to the documentation).

To find where it is defined... I guess you're going to need grep unfortunately, Locate does not work for tactics names it seems.

Upvotes: 4

Related Questions