Performance
There are some hints here (dead link)
Try Typeclasses eauto.
Be careful with coercions. They're incredibly useful, but can lead to a great deal of unnecessary work during the convertibility check. Take a look at Print Graph and try to prune it down to the minimum amount you need.
Try using the abstract tactic.
See these hints for debugging a slow Qed
See also this thread (bad link: 522 error) regarding memory consumption.
If you have your development in a single large file, try breaking it into multiple files.
Even if your machine has ample memory, reducing memory consumption can speed up proof checking (due to garbage collection?)
The Opaque/Transparent distinction is important for keeping memory consumption under control. Subproofs wrapped in the abstract tactic and proofs which end with Qed are opaque; all others are transparent (unless made opaque with the Opaque command).
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.