---
- branch: MAIN
  date: Sun Nov 14 20:53:03 UTC 2010
  files:
  - new: '1.27'
    old: '1.26'
    path: pkgsrc/lang/coq/Makefile
    pathrev: pkgsrc/lang/coq/Makefile@1.27
    type: modified
  - new: '1.11'
    old: '1.10'
    path: pkgsrc/lang/coq/PLIST
    pathrev: pkgsrc/lang/coq/PLIST@1.11
    type: modified
  - new: '1.1'
    old: '0'
    path: pkgsrc/lang/coq/PLIST.natdynlink
    pathrev: pkgsrc/lang/coq/PLIST.natdynlink@1.1
    type: added
  - new: '1.7'
    old: '1.6'
    path: pkgsrc/lang/coq/PLIST.opt
    pathrev: pkgsrc/lang/coq/PLIST.opt@1.7
    type: modified
  - new: '1.12'
    old: '1.11'
    path: pkgsrc/lang/coq/distinfo
    pathrev: pkgsrc/lang/coq/distinfo@1.12
    type: modified
  - new: '1.9'
    old: '1.8'
    path: pkgsrc/lang/coq/patches/patch-aa
    pathrev: pkgsrc/lang/coq/patches/patch-aa@1.9
    type: modified
  - new: '1.4'
    old: '1.3'
    path: pkgsrc/lang/coq/patches/patch-ab
    pathrev: pkgsrc/lang/coq/patches/patch-ab@1.4
    type: modified
  - new: '1.2'
    old: '1.1'
    path: pkgsrc/lang/coq/patches/patch-ac
    pathrev: pkgsrc/lang/coq/patches/patch-ac@1.2
    type: modified
  - new: '0'
    old: '1.1'
    path: pkgsrc/lang/coq/patches/patch-ad
    pathrev: pkgsrc/lang/coq/patches/patch-ad@0
    type: deleted
  id: 20101114T205303Z.899e7104c63e8a027062a5fa55a6fd78d3b951d5
  log: |
    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.
  module: pkgsrc
  subject: 'CVS commit: pkgsrc/lang/coq'
  unixtime: '1289767983'
  user: tonio