diff options
| author | jaapb <jaapb@pkgsrc.org> | 2017-09-08 17:19:01 +0000 |
|---|---|---|
| committer | jaapb <jaapb@pkgsrc.org> | 2017-09-08 17:19:01 +0000 |
| commit | fcaa7af19143fdc6b9703f3c4f2980197a0abfa7 (patch) | |
| tree | f13b3f6aa9ce2c94014792c5f130d20dbaecde70 /lang/coq/distinfo | |
| parent | 01d5bc902ca6d84d37e583b3afedcd0dc02a6783 (diff) | |
| download | pkgsrc-fcaa7af19143fdc6b9703f3c4f2980197a0abfa7.tar.gz | |
Updated package to latest version, 8.6.1. Changes include:
- Fix #5380: Default colors for CoqIDE are actually applied.
- Fix plugin warnings
- Document named evars (including Show ident)
- Fix Bug #5574, document function scope
- Adding a test case as requested in bug 5205.
- Fix Bug #5568, no dup notation warnings on repeated module imports
- Fix documentation of Typeclasses eauto :=
- Refactor documentation of records.
- Protecting from warnings while compiling 8.6
- Fixing an inconsistency between configure and configure.ml
- Add test-suite checks for coqchk with constraints
- Fix bug #5019 (looping zify on dependent types)
- Fix bug 5550: "typeclasses eauto with" does not work with section variables.
- Bug 5546, qualify datatype constructors when needed in Show Match
- Bug #5535, test for Show with -emacs
- Fix bug #5486, don't reverse ids in tuples
- Fixing #5522 (anomaly with free vars of pat)
- Fix bug #5526, don't check for nonlinearity in notation if printing only
- Fix bug #5255
- Fix bug #3659: -time should understand multibyte encodings.
- FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print Assumptions".
- Fix outdated description in RefMan.
- Repairing `Set Rewriting Schemes`
- Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
- Fix description of command-line arguments for Add (Rec) LoadPath
- Fix bug #5377: @? patterns broken.
- add XML protocol doc
- Fix anomaly when doing [all:Check _.] during a proof.
- Correction of bug #4306
- Fix #5435: [Eval native_compute in] raises anomaly.
- Instances should obey universe binders even when defined by tactics.
- Intern names bound in match patterns
- funind: Ignore missing info for current function
- Do not typecheck twice the type of opaque constants.
- show unused intro pattern warning
- [future] Be eager when "chaining" already resolved future values.
- Opaque side effects
- Fix #5132: coq_makefile generates incorrect install goal
- Run non-tactic comands without resilient_command
- Univs: fix bug #5365, generation of u+k <= v constraints
- make `emit' tail recursive
- Don't require printing-only notation to be productive
- Fix the way setoid_rewrite handles bindings.
- Fix for bug 5244 - set printing width ignored when given enough space
- Fix bug 4969, autoapply was not tagging shelved subgoals correctly
Diffstat (limited to 'lang/coq/distinfo')
| -rw-r--r-- | lang/coq/distinfo | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lang/coq/distinfo b/lang/coq/distinfo index 4b3bfc77824..5f09c916acc 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,8 +1,8 @@ -$NetBSD: distinfo,v 1.26 2016/12/30 13:23:06 jaapb Exp $ +$NetBSD: distinfo,v 1.27 2017/09/08 17:19:01 jaapb Exp $ -SHA1 (coq-8.6.tar.gz) = 617a6f86d09dde0e409f3fa22268daf7be3f5bba -RMD160 (coq-8.6.tar.gz) = 3d5e539c40732620e65f28988b118d2e0d663aa5 -SHA512 (coq-8.6.tar.gz) = 9f5f4913fda8cf83683fec9398b42d4567207c3d4b52b4638d5e09a24ed25a43905fb57a9fac1bb9f9d681bd47f3560e1da74e79348b3a3fd93e2e8c686cebae -Size (coq-8.6.tar.gz) = 5538848 bytes +SHA1 (coq-8.6.1.tar.gz) = 5dbaf1230c297d7c11c8715c012300a51ad80f9a +RMD160 (coq-8.6.1.tar.gz) = 822b0061a99de144881b1f1166eef9e92d26de7f +SHA512 (coq-8.6.1.tar.gz) = 814ab76a06ca15f927081428da74add4bc67290199fa011853b9c68a00cdefaf813b10fbac18a434f4504fce8f2173eb544080bf6f50d62caa41bb8724b13083 +Size (coq-8.6.1.tar.gz) = 5588811 bytes SHA1 (patch-Makefile.common) = 79b02edff66ddcfb267816b0031c724620e67a13 SHA1 (patch-configure.ml) = 8e48a65709234281e3898ebae9041dfc04c7fe7b |