• Jean-Marc Notin: A new infrastructure for Coq user contributions
• Pierre Boutillier: parsing "match" patterns like terms are parsed
• Discussion about 8.4
• Reference Manual