summaryrefslogtreecommitdiff
path: root/databases/Makefile
diff options
context:
space:
mode:
authortonio <tonio@pkgsrc.org>2010-11-14 20:53:02 +0000
committertonio <tonio@pkgsrc.org>2010-11-14 20:53:02 +0000
commit6272e8df4b9d77f3125b18494588dca4e71f72be (patch)
tree7e12c64534f3e06f29c91c6c85da9e7d72e962b3 /databases/Makefile
parentd56681405287840c99347ff33645e81209fc07e5 (diff)
downloadpkgsrc-6272e8df4b9d77f3125b18494588dca4e71f72be.tar.gz
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.
Diffstat (limited to 'databases/Makefile')
0 files changed, 0 insertions, 0 deletions