During the Cocorico redesign the following articles were moved "off the beaten path." Many are still quite informative, and with a little polish should be ready for the main page. Please consider updating and moving any articles you find useful.
Coq Pearls
QuickSort: an implementation of quicksort in Coq.
Another QuickSort: an implementation of quicksort in Coq using Program and definitions from the standard library.
InductiveFiniteTypes or alternatively FixpointFiniteTypes.
ListOfPredecessors for binary numbers.
A proof of Lagrange's Theorem.
A proof that there are not finitely many primes.
Miscellany
A discussion about Coq Style.
A discussion suggesting preferring Set to Prop.
What is the difference between Require Import and Require Export?
Isn't IntensionalEquality useless?
Do objects living in Prop ever need to be evaluated? See PropsGuardingIotaReduction.
A discussion about intensional equality.
Information about Coq's source code.