• Discussion on the standard library of Coq
• Organisational aspects
• Overall consistency and maintenance
• Compatibility issues
• Lack of Coq support for features
• Documentation and metadata issues
• Specific issues with the libraries of Coq
• Arithmetic
• General issues about arithmetic
• Peano numbers
• Binary natural numbers
• Binary integers
• Rational numbers
• Real numbers
• Lists
• Lists annotated with their length (vectors)
• Boolean
• Strings
• Logic
• Sorting
• Maps and sets (data structures)
• Relations and sets
• Unexploited content of the support for tactics (ring, ...)
• Algebra
• Libraries not represented in Coq