---
- branch: MAIN
  date: Sat Apr 25 13:41:18 UTC 2015
  files:
  - new: '1.80'
    old: '1.79'
    path: pkgsrc/lang/coq/Makefile
    pathrev: pkgsrc/lang/coq/Makefile@1.80
    type: modified
  - new: '1.16'
    old: '1.15'
    path: pkgsrc/lang/coq/PLIST
    pathrev: pkgsrc/lang/coq/PLIST@1.16
    type: modified
  - new: '1.21'
    old: '1.20'
    path: pkgsrc/lang/coq/distinfo
    pathrev: pkgsrc/lang/coq/distinfo@1.21
    type: modified
  - new: '0'
    old: '1.1'
    path: pkgsrc/lang/coq/patches/patch-kernel_univ.ml
    pathrev: pkgsrc/lang/coq/patches/patch-kernel_univ.ml@0
    type: deleted
  id: 20150425T134118Z.2db34ec44d6832b5e9d52ea3eebcd61133bf8a98
  log: |
    Updated coq to version 8.4pl6. Changes from previous version include (apart
    from bugfixes):

    - Coq compilation made possible with forthcoming ocaml 4.03.
    - command for locating exists notation in refman changed.
    - Various improvements of the Reference Manual (especially its html version)
    - implicit arguments of local definitions fixed (possible
      source of incompatibilities).
    - New command "Print Debug GC".
    - Function cannot define graph.
    - Optimizing compilation of pattern matching.
    - Better inference of impossible cases in pattern-matching.
    - Evar leak in pattern-matching compilation
    - ill-typed replacement in "change ... with ...".
    - unbound evars in "change ... with ...".
    - wrong return clause of a match pattern in Ltac.
    - cleared local hints for autounfold.
    - cleared local hints for autounfold.
    - lost evars in "change ... with ...".
    - supporting let-ins in constructors for vm_compute
    - unfortunate typo in compare_height.
    - unfortunate typos in absorption lemmas over bool.
    - Full support of utf8 Greek letters (block U0370) in coqdoc
  module: pkgsrc
  subject: 'CVS commit: pkgsrc/lang/coq'
  unixtime: '1429969278'
  user: jaapb