Coq Tactics in Plain English

charlesaverill.github.iosite

Guide to Coq tactics with explanations and examples.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲

   Official Coq manual coq.inria.fr

   site link ↗
   site
2. ▲

   Tactician coq-tactician.github.io

   Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully.

   site topic math link ↗
   site
3. ▲

   Coq'Art Exercises and Tutorials github.com

   Coq code and exercises from the Coq'Art book, including additional tutorials.

   tool topic books & writing link ↗
   
4. ▲

   Tricks in Coq github.com

   Tips, tricks, and features in Coq that are hard to discover.

   tool link ↗
   
5. ▲

   Official Coq wiki github.com

   site link ↗
   site
6. ▲

   Ltac2 coq.inria.fr

   Experimental typed tactic language similar to Coq's classic Ltac language.

   site link ↗
   site

Coq › Resources > Tutorials and Hints: “Guide to Coq tactics with explanations and examples.”