pkgsrc-Changes archive

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]

CVS commit: pkgsrc/lang/coq



Module Name:    pkgsrc
Committed By:   tonio
Date:           Sun Nov 14 20:53:03 UTC 2010

Modified Files:
        pkgsrc/lang/coq: Makefile PLIST PLIST.opt distinfo
        pkgsrc/lang/coq/patches: patch-aa patch-ab patch-ac
Added Files:
        pkgsrc/lang/coq: PLIST.natdynlink
Removed Files:
        pkgsrc/lang/coq/patches: patch-ad

Log Message:
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.


To generate a diff of this commit:
cvs rdiff -u -r1.26 -r1.27 pkgsrc/lang/coq/Makefile
cvs rdiff -u -r1.10 -r1.11 pkgsrc/lang/coq/PLIST
cvs rdiff -u -r0 -r1.1 pkgsrc/lang/coq/PLIST.natdynlink
cvs rdiff -u -r1.6 -r1.7 pkgsrc/lang/coq/PLIST.opt
cvs rdiff -u -r1.11 -r1.12 pkgsrc/lang/coq/distinfo
cvs rdiff -u -r1.8 -r1.9 pkgsrc/lang/coq/patches/patch-aa
cvs rdiff -u -r1.3 -r1.4 pkgsrc/lang/coq/patches/patch-ab
cvs rdiff -u -r1.1 -r1.2 pkgsrc/lang/coq/patches/patch-ac
cvs rdiff -u -r1.1 -r0 pkgsrc/lang/coq/patches/patch-ad

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.



Home | Main Index | Thread Index | Old Index