CVS log for pkgsrc/lang/coq/PLIST.natdynlink

Up to [cvs.netbsd.org] / pkgsrc / lang / coq

Request diff between arbitrary revisions

Default branch: MAIN

Revision 1.1 / (download) - annotate - [select for diffs], Sun Nov 14 20:53:02 2010 UTC (18 months, 1 week ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2012Q1-base, pkgsrc-2012Q1, pkgsrc-2011Q4-base, pkgsrc-2011Q4, pkgsrc-2011Q3-base, pkgsrc-2011Q3, pkgsrc-2011Q2-base, pkgsrc-2011Q2, pkgsrc-2011Q1-base, pkgsrc-2011Q1, pkgsrc-2010Q4-base, pkgsrc-2010Q4, HEAD

Update lang/coq to 8.3

Main changes:
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.

This form allows you to request diff's between any two revisions of a file. You may select a symbolic revision name using the selection box or you may type in a numeric name using the type-in text box.