[pkgsrc/trunk]: pkgsrc/lang/coq Updated package lang/coq to version 8.7.1.

[jaapb <jaapb%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/1165d2f777d4
branches:  trunk
changeset: 373869:1165d2f777d4
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Wed Jan 10 16:26:53 2018 +0000

description:
Updated package lang/coq to version 8.7.1.

This is a compatibility release with OCaml 4.06.0. It also contains many
bugfixes, documentation improvements and user message improvements.

diffstat:

 lang/coq/Makefile                      |    7 +-
 lang/coq/PLIST                         |  642 +++++++++++++++++++++++++++++---
 lang/coq/distinfo                      |   12 +-
 lang/coq/options.mk                    |    7 +-
 lang/coq/patches/patch-configure.ml    |   14 -
 lang/coq/patches/patch-ide_ideutils.ml |   14 -
 6 files changed, 587 insertions(+), 109 deletions(-)

diffs (truncated from 1481 to 300 lines):

diff -r d063f228ca92 -r 1165d2f777d4 lang/coq/Makefile
--- a/lang/coq/Makefile Wed Jan 10 16:24:25 2018 +0000
+++ b/lang/coq/Makefile Wed Jan 10 16:26:53 2018 +0000
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.103 2017/11/30 16:45:28 adam Exp $
+# $NetBSD: Makefile,v 1.104 2018/01/10 16:26:53 jaapb Exp $
 #
 
-DISTNAME=      coq-8.7.0
-PKGREVISION=   2
+DISTNAME=      coq-8.7.1
 CATEGORIES=    lang math
 MASTER_SITES=  http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -75,7 +74,7 @@
 SUBST_FILES.fix-paths= config/coq_config.ml
 SUBST_SED.fix-paths=   -e "s,${BUILDLINK_DIR},${PREFIX},g"
 
-
 .include "../../lang/camlp5/buildlink3.mk"
+.include "../../math/ocaml-num/buildlink3.mk"
 .include "../../mk/pthread.buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff -r d063f228ca92 -r 1165d2f777d4 lang/coq/PLIST
--- a/lang/coq/PLIST    Wed Jan 10 16:24:25 2018 +0000
+++ b/lang/coq/PLIST    Wed Jan 10 16:26:53 2018 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.23 2018/01/01 22:29:39 rillig Exp $
+@comment $NetBSD: PLIST,v 1.24 2018/01/10 16:26:53 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -13,20 +13,33 @@
 bin/gallina
 lib/coq/META
 lib/coq/config/coq_config.cmi
+${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx
 lib/coq/engine/eConstr.cmi
+${PLIST.ocaml-opt}lib/coq/engine/eConstr.cmx
 ${PLIST.ocaml-opt}lib/coq/engine/engine.a
 ${PLIST.ocaml-opt}lib/coq/engine/engine.cmxa
 lib/coq/engine/evarutil.cmi
+${PLIST.ocaml-opt}lib/coq/engine/evarutil.cmx
 lib/coq/engine/evd.cmi
+${PLIST.ocaml-opt}lib/coq/engine/evd.cmx
 lib/coq/engine/ftactic.cmi
+${PLIST.ocaml-opt}lib/coq/engine/ftactic.cmx
 lib/coq/engine/geninterp.cmi
+${PLIST.ocaml-opt}lib/coq/engine/geninterp.cmx
 lib/coq/engine/logic_monad.cmi
+${PLIST.ocaml-opt}lib/coq/engine/logic_monad.cmx
 lib/coq/engine/namegen.cmi
+${PLIST.ocaml-opt}lib/coq/engine/namegen.cmx
 lib/coq/engine/proofview.cmi
+${PLIST.ocaml-opt}lib/coq/engine/proofview.cmx
 lib/coq/engine/proofview_monad.cmi
+${PLIST.ocaml-opt}lib/coq/engine/proofview_monad.cmx
 lib/coq/engine/termops.cmi
+${PLIST.ocaml-opt}lib/coq/engine/termops.cmx
 lib/coq/engine/uState.cmi
+${PLIST.ocaml-opt}lib/coq/engine/uState.cmx
 lib/coq/engine/universes.cmi
+${PLIST.ocaml-opt}lib/coq/engine/universes.cmx
 lib/coq/grammar/grammar.cma
 lib/coq/grammar/q_util.cmi
 ${PLIST.coqide}lib/coq/ide/config_lexer.cmi
@@ -68,185 +81,343 @@
 ${PLIST.coqide}lib/coq/ide/xml_printer.cmi
 ${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
 lib/coq/interp/constrexpr_ops.cmi
+${PLIST.ocaml-opt}lib/coq/interp/constrexpr_ops.cmx
 lib/coq/interp/constrextern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/constrextern.cmx
 lib/coq/interp/constrintern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/constrintern.cmx
 lib/coq/interp/declare.cmi
+${PLIST.ocaml-opt}lib/coq/interp/declare.cmx
 lib/coq/interp/dumpglob.cmi
+${PLIST.ocaml-opt}lib/coq/interp/dumpglob.cmx
 lib/coq/interp/genintern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/genintern.cmx
 lib/coq/interp/impargs.cmi
+${PLIST.ocaml-opt}lib/coq/interp/impargs.cmx
 lib/coq/interp/implicit_quantifiers.cmi
+${PLIST.ocaml-opt}lib/coq/interp/implicit_quantifiers.cmx
 ${PLIST.ocaml-opt}lib/coq/interp/interp.a
 ${PLIST.ocaml-opt}lib/coq/interp/interp.cmxa
 lib/coq/interp/modintern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/modintern.cmx
 lib/coq/interp/notation.cmi
+${PLIST.ocaml-opt}lib/coq/interp/notation.cmx
 lib/coq/interp/notation_ops.cmi
+${PLIST.ocaml-opt}lib/coq/interp/notation_ops.cmx
 lib/coq/interp/ppextend.cmi
+${PLIST.ocaml-opt}lib/coq/interp/ppextend.cmx
 lib/coq/interp/reserve.cmi
+${PLIST.ocaml-opt}lib/coq/interp/reserve.cmx
 lib/coq/interp/smartlocate.cmi
+${PLIST.ocaml-opt}lib/coq/interp/smartlocate.cmx
 lib/coq/interp/stdarg.cmi
+${PLIST.ocaml-opt}lib/coq/interp/stdarg.cmx
 lib/coq/interp/syntax_def.cmi
+${PLIST.ocaml-opt}lib/coq/interp/syntax_def.cmx
 lib/coq/interp/topconstr.cmi
+${PLIST.ocaml-opt}lib/coq/interp/topconstr.cmx
 lib/coq/intf/constrexpr.cmi
+${PLIST.ocaml-opt}lib/coq/intf/constrexpr.cmx
 lib/coq/intf/decl_kinds.cmi
+${PLIST.ocaml-opt}lib/coq/intf/decl_kinds.cmx
 lib/coq/intf/evar_kinds.cmi
+${PLIST.ocaml-opt}lib/coq/intf/evar_kinds.cmx
 lib/coq/intf/extend.cmi
+${PLIST.ocaml-opt}lib/coq/intf/extend.cmx
 lib/coq/intf/genredexpr.cmi
+${PLIST.ocaml-opt}lib/coq/intf/genredexpr.cmx
 lib/coq/intf/glob_term.cmi
+${PLIST.ocaml-opt}lib/coq/intf/glob_term.cmx
 ${PLIST.ocaml-opt}lib/coq/intf/intf.a
 ${PLIST.ocaml-opt}lib/coq/intf/intf.cmxa
 lib/coq/intf/locus.cmi
+${PLIST.ocaml-opt}lib/coq/intf/locus.cmx
 lib/coq/intf/misctypes.cmi
+${PLIST.ocaml-opt}lib/coq/intf/misctypes.cmx
 lib/coq/intf/notation_term.cmi
+${PLIST.ocaml-opt}lib/coq/intf/notation_term.cmx
 lib/coq/intf/pattern.cmi
+${PLIST.ocaml-opt}lib/coq/intf/pattern.cmx
 lib/coq/intf/tactypes.cmi
+${PLIST.ocaml-opt}lib/coq/intf/tactypes.cmx
 lib/coq/intf/vernacexpr.cmi
+${PLIST.ocaml-opt}lib/coq/intf/vernacexpr.cmx
 lib/coq/kernel/byterun/dllcoqrun.so
-lib/coq/kernel/byterun/libcoqrun.a
+${PLIST.ocaml-opt}lib/coq/kernel/byterun/libcoqrun.a
 lib/coq/kernel/cClosure.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cClosure.cmx
 lib/coq/kernel/cbytecodes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cbytecodes.cmx
 lib/coq/kernel/cbytegen.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cbytegen.cmx
 lib/coq/kernel/cemitcodes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cemitcodes.cmx
 lib/coq/kernel/constr.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/constr.cmx
 lib/coq/kernel/context.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/context.cmx
 lib/coq/kernel/conv_oracle.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/conv_oracle.cmx
 lib/coq/kernel/cooking.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cooking.cmx
 lib/coq/kernel/copcodes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/copcodes.cmx
 lib/coq/kernel/csymtable.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/csymtable.cmx
 lib/coq/kernel/declarations.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/declarations.cmx
 lib/coq/kernel/declareops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/declareops.cmx
 lib/coq/kernel/entries.cmi
 lib/coq/kernel/environ.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/environ.cmx
 lib/coq/kernel/esubst.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/esubst.cmx
 lib/coq/kernel/evar.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/evar.cmx
 lib/coq/kernel/indtypes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/indtypes.cmx
 lib/coq/kernel/inductive.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/inductive.cmx
 ${PLIST.ocaml-opt}lib/coq/kernel/kernel.a
 ${PLIST.ocaml-opt}lib/coq/kernel/kernel.cmxa
 lib/coq/kernel/mod_subst.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/mod_subst.cmx
 lib/coq/kernel/mod_typing.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/mod_typing.cmx
 lib/coq/kernel/modops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/modops.cmx
 lib/coq/kernel/names.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/names.cmx
 lib/coq/kernel/nativecode.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativecode.cmx
 lib/coq/kernel/nativeconv.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativeconv.cmx
 lib/coq/kernel/nativeinstr.cmi
 lib/coq/kernel/nativelambda.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativelambda.cmx
 lib/coq/kernel/nativelib.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativelib.cmx
 lib/coq/kernel/nativelibrary.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativelibrary.cmx
 lib/coq/kernel/nativevalues.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativevalues.cmx
 lib/coq/kernel/opaqueproof.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/opaqueproof.cmx
 lib/coq/kernel/pre_env.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/pre_env.cmx
 lib/coq/kernel/primitives.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/primitives.cmx
 lib/coq/kernel/reduction.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/reduction.cmx
 lib/coq/kernel/retroknowledge.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/retroknowledge.cmx
 lib/coq/kernel/safe_typing.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/safe_typing.cmx
 lib/coq/kernel/sorts.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/sorts.cmx
 lib/coq/kernel/subtyping.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/subtyping.cmx
 lib/coq/kernel/term.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/term.cmx
 lib/coq/kernel/term_typing.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/term_typing.cmx
 lib/coq/kernel/type_errors.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/type_errors.cmx
 lib/coq/kernel/typeops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/typeops.cmx
 lib/coq/kernel/uGraph.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/uGraph.cmx
 lib/coq/kernel/uint31.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/uint31.cmx
 lib/coq/kernel/univ.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/univ.cmx
 lib/coq/kernel/vars.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/vars.cmx
 lib/coq/kernel/vconv.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/vconv.cmx
 lib/coq/kernel/vm.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/vm.cmx
 lib/coq/lib/aux_file.cmi
+${PLIST.ocaml-opt}lib/coq/lib/aux_file.cmx
 lib/coq/lib/backtrace.cmi
+${PLIST.ocaml-opt}lib/coq/lib/backtrace.cmx
 lib/coq/lib/bigint.cmi
+${PLIST.ocaml-opt}lib/coq/lib/bigint.cmx
 lib/coq/lib/cArray.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cArray.cmx
 lib/coq/lib/cAst.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cAst.cmx
 lib/coq/lib/cEphemeron.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cEphemeron.cmx
 lib/coq/lib/cErrors.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cErrors.cmx
 lib/coq/lib/cList.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cList.cmx
 lib/coq/lib/cMap.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cMap.cmx
 lib/coq/lib/cObj.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cObj.cmx
 lib/coq/lib/cSet.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cSet.cmx
 lib/coq/lib/cSig.cmi
 lib/coq/lib/cStack.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cStack.cmx
 lib/coq/lib/cString.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cString.cmx
 lib/coq/lib/cThread.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cThread.cmx
 lib/coq/lib/cUnix.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cUnix.cmx
 lib/coq/lib/cWarnings.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cWarnings.cmx
 lib/coq/lib/canary.cmi
+${PLIST.ocaml-opt}lib/coq/lib/canary.cmx
 ${PLIST.ocaml-opt}lib/coq/lib/clib.a
 ${PLIST.ocaml-opt}lib/coq/lib/clib.cmxa
 lib/coq/lib/control.cmi
+${PLIST.ocaml-opt}lib/coq/lib/control.cmx
 lib/coq/lib/coqProject_file.cmi
+${PLIST.ocaml-opt}lib/coq/lib/coqProject_file.cmx
 lib/coq/lib/deque.cmi
+${PLIST.ocaml-opt}lib/coq/lib/deque.cmx
 lib/coq/lib/dyn.cmi
+${PLIST.ocaml-opt}lib/coq/lib/dyn.cmx
 lib/coq/lib/envars.cmi
+${PLIST.ocaml-opt}lib/coq/lib/envars.cmx
 lib/coq/lib/exninfo.cmi
+${PLIST.ocaml-opt}lib/coq/lib/exninfo.cmx
 lib/coq/lib/explore.cmi
+${PLIST.ocaml-opt}lib/coq/lib/explore.cmx
 lib/coq/lib/feedback.cmi
+${PLIST.ocaml-opt}lib/coq/lib/feedback.cmx
 lib/coq/lib/flags.cmi
+${PLIST.ocaml-opt}lib/coq/lib/flags.cmx
 lib/coq/lib/future.cmi
+${PLIST.ocaml-opt}lib/coq/lib/future.cmx
 lib/coq/lib/genarg.cmi
+${PLIST.ocaml-opt}lib/coq/lib/genarg.cmx
 lib/coq/lib/hMap.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hMap.cmx
 lib/coq/lib/hashcons.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hashcons.cmx
 lib/coq/lib/hashset.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hashset.cmx
 lib/coq/lib/heap.cmi
+${PLIST.ocaml-opt}lib/coq/lib/heap.cmx
 lib/coq/lib/hook.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hook.cmx
 lib/coq/lib/iStream.cmi
+${PLIST.ocaml-opt}lib/coq/lib/iStream.cmx
 lib/coq/lib/int.cmi