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: jaapb
Date: Sat Apr 25 13:41:18 UTC 2015
Modified Files:
pkgsrc/lang/coq: Makefile PLIST distinfo
Removed Files:
pkgsrc/lang/coq/patches: patch-kernel_univ.ml
Log Message:
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
To generate a diff of this commit:
cvs rdiff -u -r1.79 -r1.80 pkgsrc/lang/coq/Makefile
cvs rdiff -u -r1.15 -r1.16 pkgsrc/lang/coq/PLIST
cvs rdiff -u -r1.20 -r1.21 pkgsrc/lang/coq/distinfo
cvs rdiff -u -r1.1 -r0 pkgsrc/lang/coq/patches/patch-kernel_univ.ml
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