The main features of Coq version 8.1 are

- the implementation of an alternative algorithm for checking the
  convertibility of types, specially dedicated to fast type-checking
  of reflexion-based proofs, and more generally to intensive
  computation

- richer inductive types

  - support for recursively non uniform parameters
  - support for a strong form of sort-polymorphism

- improved tactics

  - new implementation of setoid rewrite (contributed by C. Sacerdoti Coen)
  - new implementation of ring (contributed by B. Grégoire and A. Mahboubi)
  - and several other new tactic features

- new libraries
 
  - finite sets and finite maps (by J.-C. Filliâtre and P. Letouzey)
  - strings (by L. Théry)
  - significative extensions of the library on lists
  - a few other extensions

- improved module system