• High-level language
• Syntax of terms
• Support for custom numeral notations
• Support for specific constr grammar entries
• A more expressive language for Coq binders
• Induction schemes
• Extended detection of computationally-void inductive propositions
• Total ordering of algebraic data-types
• Equality induction principle for records
• Coercions
• Tactics
• Simplification tactics
• Injection
• Rewriting
• Discriminate
• Specialize
• Referring to hypotheses by type
• Optimizations
• Unification
• Inversion combined with recursion
• The Ltac language
• The Calculus of Inductive Constructions
• Support lexicographic termination in Fixpoint
• Support refolding of fixpoints in the kernel
• Dependent mutual fixpoints
• Recognizing uniform parameters in fixpoints
• Per-inductive parameters in mutual inductive blocks
• Generalizing positivity condition
• Investigation into commutative cuts
• Making transparent the body of an opaque constant
• Coqdoc
• Features
• Support links from within [...] parts of comments
• Index
• Output independant layout language
• Native output format