aboutsummaryrefslogtreecommitdiffhomepage
path: root/ANNONCE
blob: 5e634f2cb80c432ed9e74ae5425b7d8d5f208dcd (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
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