• Points discussed for integration to Coq 8.5
• New-tacticals (Arnaud)
• Asynchronous lazy evaluation of commands (Enrico)
• Full polymorphism of universes (Matthieu)
• Ad hoc representation of projections in the code (Matthieu)
• Hack for not doing intensive computations both at proof time and qed time (Enrico)
• Coqdoc (Yann)
• Miscellaneous discussions
• Reduction of vo size with modules (Letouzey)
• Introduction of a proper intropattern notation for injecting an equality on the fly (Hugo)
• Compilation of user contributions and test-suite