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