Skip to the content.

Tricks in Coq

Docker CI Contributing Code of Conduct Zulip

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

If you have a trick you’ve found useful feel free to submit an issue or pull request!

Meta

To build all the examples in src/, run make.

Ltac

Gallina

Other Coq commands

Warnings and options

Using Coq