Home

Coq 8.3 is out !

Submitted by coq-www on 14 Oct 2010 16:45 GMT

We are pleased to announce the final release of Coq 8.3 which includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that extends ring to systems of polynomial equations) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated).

This version also comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. Here is an excerpt:

  • new operator <+ for conveniently chaining application of functors
  • new round of extension of the modular library of arithmetic
  • support for matching terms with binders in Ltac,
  • linking notations in coqdoc,
  • quote tactic now working on arbitrary expressions,
  • Lemma and co accept parameters that are automatically introduced,
  • interactive proofs in module types,
  • a beautifying coqc option for pretty-printing files

See the file CHANGES for a full log of changes.

Even if we try to preserve compatibility as much as possible with Coq 8.2, we had to arbitrate for a break of behavior in some situations. The major incompatibilities can be easily treated by using the new -compat 8.2 option or by setting/unsetting adequate options. See COMPATIBILITY for details and migration recommendations.

In addition to the "ssreflect" plugin, extension packages we are aware about include the following (but probably there are more):

  • the Heq library for smooth rewriting using heterogeneous equality by C.-K. Hur;
  • the aac_tactics plugin for rewriting modulo associativity and commutativity by T. Braibant and D. Pous.

Note also the following user contributions submitted since 8.2 was released:

  • Projective geometry in plane and space (N. Magaud, J. Narboux, P. Schreck)
  • Proofs of Quicksort's worst- and average-case complexity (Eelis)
  • Tactic that helps to prove inductive lemmas by fixpoint "descente infinie" functions (M. Li)
  • A tactic for deciding Kleene algebras (T. Braibant and D. Pous)

If you want to try it, go to the download page.

The Coq development team