The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Coq-Club members,

The final release of Coq 8.3 is available for a few weeks already now
at http://coq.inria.fr/download and here comes the official announcement.

The main novelties are a new decision tactic "nsatz" (standing for
Hilbert's NullStellensatz and extending "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).

The 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 http://coq.inria.fr/V8.3/CHANGES for a full log of changes.

Even if we reasonably tried to preserve compatibility 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 http://coq.inria.fr/V8.3/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)

The Coq development team