The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Dear all,

I am pleased to announce a new release of CoLoR (color.1.2.0 on opam) 
that compiles with Coq 8.5 whose main changes wrt the previous release 
(1.1.0 in March 2015) are:

- Util/Relation/Tarski: induction principle for the least fixpoint of a 
monotone function
- Term/Lambda/LEta: eta-reduction in pure lambda-calculus
- Term/Lambda/LComp: generalization of the computability axioms for 
handling eta-reduction

Some elements have been renamed or moved around, and others added.
Improvements in some proof scripts led to a 18% decrease of the 
compilation time (with Coq 8.4pl6).

More details can be found on http://color.gforge.inria.fr/.

Frédéric.