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
|
