• Organisation
• Talks
• Talking points
• Participants
• Presentation of the new Jedit interface to Coq by Carst Tankink
• Guard condition
• Proposal for a revision of the TACTIC EXTEND model by Pierre-Marie Pédrot
• Patch from Pierre-Marie Pédrot about drastically reducing time in univ.ml
• Code cleaning
• Presentation of the syntax for explicit universes by Matthieu Sozeau
• New bench/web server
• Auxiliary data storage and installation
• About the Coq public service
• User contributions
• Release process