• Debugging output for tactics
• Can commutativity of or be proven?
• Syntax Question: What does ... mean?
• Operational Semantics of Coq
• Implicit arguments
• From Coq proof scripts to declarative proofs?