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/Makefile | |
| 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/Makefile')
| -rw-r--r-- | lang/coq/Makefile | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 288f4ec367c..52a945dfebf 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -1,8 +1,7 @@ -# $NetBSD: Makefile,v 1.98 2017/07/11 14:19:20 jaapb Exp $ +# $NetBSD: Makefile,v 1.99 2017/09/08 17:19:01 jaapb Exp $ # -DISTNAME= coq-8.6 -PKGREVISION= 4 +DISTNAME= coq-8.6.1 CATEGORIES= lang math MASTER_SITES= http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/ @@ -26,10 +25,15 @@ BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10 .include "../../mk/bsd.prefs.mk" .include "../../mk/ocaml.mk" +PLIST_VARS+= native .if ${OCAML_USE_OPT_COMPILER} == "yes" PLIST_SUBST+= COQIDE_TYPE="opt" +PLIST.native= yes +CONFIGURE_ARGS+= -native-compiler yes +UNLIMIT_RESOURCES+= stacksize # compilation of some files needs this .else PLIST_SUBST+= COQIDE_TYPE="byte" +CONFIGURE_ARGS+= -native-compiler no .endif .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64") |