Cocorico Main Page (V2)
HighLevel Advice and Guidance
Beginners Video Tutorials by Andrej Bauer
How do I do mutual induction?
How should I organize large inductive proofs?
How do I do induction over a type containing pairs?
Where else can I learn about Coq?
Where can I read research papers about Coq's theoretical foundations?
How can use the module system effectively?
What tools and tactic packages are available for Coq?
Where can I learn about proofs for languages with variable binding?
How can I get better Performance out of Coq?
What hints can you give me about Extraction of OCaml/Haskell/Scheme code?
How can I do induction with self defined cases ?
How do TypeClasses work?
How do ImplicitArguments work?
How can I input unicode characters for Coq independently of my editor using XCompose (X graphical servers only) or the TeX input method (Unix systems).
Community
Who is using Coq in their programming languages research?
Who is using Coq for the formalization of mathematics?
How is Coq being taught and used to teach?
Language Constructs and BuiltIn Tactics
What exactly does simpl do?
How can I avoid noninstantiated existential variables with eauto?
How does the pattern match syntax work?
How does dependent inversion work?
When using eapply, how can I instantiate the question marks?
How can I make Coq always print universes?
Why doesn't Coq support extension equality? (Why can't I prove forall x, f x = g x) > f = g?)
Why does Coq use inductive types and not WTypes?
Why can I eliminate False (a Prop) when constructing a member of Set?
How does the fix tactic work?
Why do I get "Error: Abstracting over the term ... leads to a term which is illtyped" when rewriting with equalities?
Some Useful Custom Tactics and Notation
Automatically cleaning your hypothesis like in linear programming (contains also an example of a way to have list of hypothesis in a custom tactic)
A simple example of a tactic written in OCaml
Unfold a fixpoint once (in OCaml)
Formal Developments and Coq Pearls
SquareRootTwo: A very short proof that the square root of 2 is non rational.
UntypedLambdaTerms: various data structures for implementing the untyped lambda calculus in Coq.
QuickSort: an implementation of quicksort in Coq using Program.
ExistsFromPropToSet: Existential implies Sigma for decidable properties on nat.
HandMul: A fun way of doing multiplication by hand
Math Classes: Mathematics using TypeClasses
Where can I see other examples of formalization and verification?
ProofGeneral and CoqIDE Tips
How do I change the Proof General Error Color?
I'm using Proof General. Where did my proof state go?
Meta
Where is the old front page?
Where can I learn about this wiki?
How do I edit this wiki?
Where did that old article go?
Cocorico Main Page (V1)
This site is a WikiWikiWeb dedicated to the Coq proof assistant.
The Coq Community 
Documentation 
Formalisations 
Software 








