diff options
author | jaapb <jaapb@pkgsrc.org> | 2020-01-24 15:54:48 +0000 |
---|---|---|
committer | jaapb <jaapb@pkgsrc.org> | 2020-01-24 15:54:48 +0000 |
commit | f0e5d4172f6e8d2a09c5d3e7967ed0deca10b861 (patch) | |
tree | d4dd591898acc88ed9f332b9c6d7b0749eed1d44 /lang/coq | |
parent | bb0fcd32fbe41f05314735f1402e6dd88ec8997c (diff) | |
download | pkgsrc-f0e5d4172f6e8d2a09c5d3e7967ed0deca10b861.tar.gz |
Updated lang/coq to version 8.10.2.
Changes include:
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositons: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
and many small improvements and bugfixes.
Diffstat (limited to 'lang/coq')
-rw-r--r-- | lang/coq/Makefile | 18 | ||||
-rw-r--r-- | lang/coq/PLIST | 235 | ||||
-rw-r--r-- | lang/coq/distinfo | 13 | ||||
-rw-r--r-- | lang/coq/options.mk | 7 | ||||
-rw-r--r-- | lang/coq/patches/patch-Makefile.build | 15 | ||||
-rw-r--r-- | lang/coq/patches/patch-Makefile.common | 3 |
6 files changed, 175 insertions, 116 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 75c49bddf3a..c242bdc8157 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -1,18 +1,17 @@ -# $NetBSD: Makefile,v 1.127 2020/01/18 21:49:42 jperkin Exp $ +# $NetBSD: Makefile,v 1.128 2020/01/24 15:54:48 jaapb Exp $ # -DISTNAME= coq-8.9.1 -PKGREVISION= 4 +DISTNAME= coq-8.10.2 CATEGORIES= lang math MASTER_SITES= ${MASTER_SITE_GITHUB:=coq/} GITHUB_TAG= V${PKGVERSION_NOREV:S/_/+/} MAINTAINER= jaapb@NetBSD.org -HOMEPAGE= http://coq.inria.fr/ +HOMEPAGE= https://coq.inria.fr/ COMMENT= Theorem prover which extracts programs from proofs LICENSE= gnu-lgpl-v2.1 -WRKSRC= ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/_/-/} +WRKSRC= ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/+/-/} USE_TOOLS+= gmake HAS_CONFIGURE= yes @@ -22,6 +21,7 @@ CONFIGURE_ARGS+= -mandir ${PREFIX}/${PKGMANDIR} CONFIGURE_ARGS+= -configdir ${PKG_SYSCONFDIR}/xdg/coq CONFIGURE_ARGS+= -docdir ${PREFIX}/share/doc/coq CONFIGURE_ARGS+= -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq +CONFIGURE_ARGS+= -flambda-opts '-O3 -unbox-closures' BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10 @@ -30,17 +30,18 @@ BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10 PLIST_VARS+= native .if ${OCAML_USE_OPT_COMPILER} == "yes" -PLIST_SUBST+= COQIDE_TYPE="opt" +COQIDE_TYPE= opt PLIST.native= yes CONFIGURE_ARGS+= -native-compiler yes UNLIMIT_RESOURCES+= stacksize # compilation of some files needs this BUILD_TARGET= world .else -PLIST_SUBST+= COQIDE_TYPE="byte" +COQIDE_TYPE= byte CONFIGURE_ARGS+= -native-compiler no BUILD_TARGET= byte INSTALL_TARGET= install-byte .endif +PLIST_SUBST+= COQIDE_TYPE=${COQIDE_TYPE} .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64") . if !empty(MACHINE_PLATFORM:MLinux-*-*) || \ @@ -56,7 +57,7 @@ PLIST.natdynlink= yes REPLACE_SH= configure install.sh REPLACE_INTERPRETER= python -REPLACE.python.old= python +REPLACE.python.old= python3 REPLACE.python.new= ${PYTHONBIN} REPLACE_FILES.python= tools/TimeFileMaker.py \ tools/make-both-single-timing-files.py \ @@ -78,7 +79,6 @@ SUBST_MESSAGE.fix-paths= Remove buildlink references from Coq_config module 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 --git a/lang/coq/PLIST b/lang/coq/PLIST index c7fc7aa3c91..fa833ac5be5 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -1,4 +1,4 @@ -@comment $NetBSD: PLIST,v 1.29 2019/03/06 09:28:23 jaapb Exp $ +@comment $NetBSD: PLIST,v 1.30 2020/01/24 15:54:48 jaapb Exp $ bin/coq-tex bin/coq_makefile bin/coqc @@ -88,6 +88,8 @@ lib/coq/clib/unicodetable.cmi ${PLIST.ocaml-opt}lib/coq/clib/unicodetable.cmx lib/coq/clib/unionfind.cmi ${PLIST.ocaml-opt}lib/coq/clib/unionfind.cmx +${PLIST.ocaml-opt}lib/coq/config/config.a +${PLIST.ocaml-opt}lib/coq/config/config.cmxa lib/coq/config/coq_config.cmi ${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx lib/coq/coqpp/coqpp_ast.cmi @@ -128,12 +130,20 @@ lib/coq/engine/univProblem.cmi ${PLIST.ocaml-opt}lib/coq/engine/univProblem.cmx lib/coq/engine/univSubst.cmi ${PLIST.ocaml-opt}lib/coq/engine/univSubst.cmx -lib/coq/engine/universes.cmi -${PLIST.ocaml-opt}lib/coq/engine/universes.cmx lib/coq/engine/univops.cmi ${PLIST.ocaml-opt}lib/coq/engine/univops.cmx -lib/coq/grammar/grammar.cma -lib/coq/grammar/q_util.cmi +${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.a +lib/coq/gramlib/.pack/gramlib.cmi +${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmx +${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmxa +lib/coq/gramlib/.pack/gramlib__Gramext.cmi +${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Gramext.cmx +lib/coq/gramlib/.pack/gramlib__Grammar.cmi +${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Grammar.cmx +lib/coq/gramlib/.pack/gramlib__Plexing.cmi +${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Plexing.cmx +lib/coq/gramlib/.pack/gramlib__Ploc.cmi +${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Ploc.cmx ${PLIST.coqide}lib/coq/ide/config_lexer.cmi ${PLIST.coqide}lib/coq/ide/configwin.cmi ${PLIST.coqide}lib/coq/ide/configwin_ihm.cmi @@ -150,12 +160,13 @@ ${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi ${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.a ${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.cmxa ${PLIST.coqide}lib/coq/ide/ideutils.cmi +${PLIST.coqide}lib/coq/ide/microPG.cmi ${PLIST.coqide}lib/coq/ide/minilib.cmi -${PLIST.coqide}lib/coq/ide/nanoPG.cmi ${PLIST.coqide}lib/coq/ide/preferences.cmi ${PLIST.coqide}lib/coq/ide/sentence.cmi ${PLIST.coqide}lib/coq/ide/session.cmi ${PLIST.coqide}lib/coq/ide/tags.cmi +${PLIST.coqide}lib/coq/ide/unicode_bindings.cmi ${PLIST.coqide}lib/coq/ide/utf8_convert.cmi ${PLIST.coqide}lib/coq/ide/wg_Command.cmi ${PLIST.coqide}lib/coq/ide/wg_Completion.cmi @@ -183,8 +194,6 @@ 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/genredexpr.cmi -${PLIST.ocaml-opt}lib/coq/interp/genredexpr.cmx lib/coq/interp/impargs.cmi ${PLIST.ocaml-opt}lib/coq/interp/impargs.cmx lib/coq/interp/implicit_quantifiers.cmi @@ -199,8 +208,8 @@ lib/coq/interp/notation_ops.cmi ${PLIST.ocaml-opt}lib/coq/interp/notation_ops.cmx lib/coq/interp/notation_term.cmi ${PLIST.ocaml-opt}lib/coq/interp/notation_term.cmx -lib/coq/interp/redops.cmi -${PLIST.ocaml-opt}lib/coq/interp/redops.cmx +lib/coq/interp/numTok.cmi +${PLIST.ocaml-opt}lib/coq/interp/numTok.cmx lib/coq/interp/reserve.cmi ${PLIST.ocaml-opt}lib/coq/interp/reserve.cmx lib/coq/interp/smartlocate.cmi @@ -221,7 +230,6 @@ 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/cinstr.cmi lib/coq/kernel/clambda.cmi ${PLIST.ocaml-opt}lib/coq/kernel/clambda.cmx lib/coq/kernel/constr.cmi @@ -248,6 +256,8 @@ 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/indTyping.cmi +${PLIST.ocaml-opt}lib/coq/kernel/indTyping.cmx lib/coq/kernel/indtypes.cmi ${PLIST.ocaml-opt}lib/coq/kernel/indtypes.cmx lib/coq/kernel/inductive.cmi @@ -266,7 +276,6 @@ 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 @@ -277,10 +286,14 @@ 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/primred.cmi +${PLIST.ocaml-opt}lib/coq/kernel/primred.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/retypeops.cmi +${PLIST.ocaml-opt}lib/coq/kernel/retypeops.cmx lib/coq/kernel/safe_typing.cmi ${PLIST.ocaml-opt}lib/coq/kernel/safe_typing.cmx lib/coq/kernel/sorts.cmi @@ -291,14 +304,16 @@ 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/transparentState.cmi +${PLIST.ocaml-opt}lib/coq/kernel/transparentState.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/uint63.cmi +${PLIST.ocaml-opt}lib/coq/kernel/uint63.cmx lib/coq/kernel/univ.cmi ${PLIST.ocaml-opt}lib/coq/kernel/univ.cmx lib/coq/kernel/vars.cmi @@ -309,6 +324,8 @@ lib/coq/kernel/vm.cmi ${PLIST.ocaml-opt}lib/coq/kernel/vm.cmx lib/coq/kernel/vmvalues.cmi ${PLIST.ocaml-opt}lib/coq/kernel/vmvalues.cmx +lib/coq/lib/acyclicGraph.cmi +${PLIST.ocaml-opt}lib/coq/lib/acyclicGraph.cmx lib/coq/lib/aux_file.cmi ${PLIST.ocaml-opt}lib/coq/lib/aux_file.cmx lib/coq/lib/cAst.cmi @@ -368,8 +385,6 @@ lib/coq/library/declaremods.cmi ${PLIST.ocaml-opt}lib/coq/library/declaremods.cmx lib/coq/library/decls.cmi ${PLIST.ocaml-opt}lib/coq/library/decls.cmx -lib/coq/library/dischargedhypsmap.cmi -${PLIST.ocaml-opt}lib/coq/library/dischargedhypsmap.cmx lib/coq/library/global.cmi ${PLIST.ocaml-opt}lib/coq/library/global.cmx lib/coq/library/globnames.cmi @@ -444,6 +459,7 @@ ${PLIST.ocaml-opt}lib/coq/plugins/btauto/btauto_plugin.cmx ${PLIST.natdynlink}lib/coq/plugins/btauto/btauto_plugin.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/btauto/btauto_plugin.o ${PLIST.ocaml-opt}lib/coq/plugins/btauto/g_btauto.cmx +lib/coq/plugins/btauto/refl_btauto.cmi ${PLIST.ocaml-opt}lib/coq/plugins/btauto/refl_btauto.cmx lib/coq/plugins/cc/cc_plugin.cmi ${PLIST.ocaml-opt}lib/coq/plugins/cc/cc_plugin.cmx @@ -502,6 +518,10 @@ lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmi ${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx ${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o +lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmi +${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmx +${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs +${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.o lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi ${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx ${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs @@ -562,6 +582,9 @@ lib/coq/plugins/extraction/ExtrHaskellZInteger.vo lib/coq/plugins/extraction/ExtrHaskellZNum.glob lib/coq/plugins/extraction/ExtrHaskellZNum.v lib/coq/plugins/extraction/ExtrHaskellZNum.vo +lib/coq/plugins/extraction/ExtrOCamlInt63.glob +lib/coq/plugins/extraction/ExtrOCamlInt63.v +lib/coq/plugins/extraction/ExtrOCamlInt63.vo lib/coq/plugins/extraction/ExtrOcamlBasic.glob lib/coq/plugins/extraction/ExtrOcamlBasic.v lib/coq/plugins/extraction/ExtrOcamlBasic.vo @@ -730,6 +753,10 @@ lib/coq/plugins/ltac/tauto_plugin.cmi ${PLIST.ocaml-opt}lib/coq/plugins/ltac/tauto_plugin.cmx ${PLIST.natdynlink}lib/coq/plugins/ltac/tauto_plugin.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/ltac/tauto_plugin.o +lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmi +${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmx +${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmxs +${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.o lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx ${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs @@ -802,6 +829,9 @@ lib/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmx ${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.o +lib/coq/plugins/micromega/DeclConstant.glob +lib/coq/plugins/micromega/DeclConstant.v +lib/coq/plugins/micromega/DeclConstant.vo lib/coq/plugins/micromega/Env.glob lib/coq/plugins/micromega/Env.v lib/coq/plugins/micromega/Env.vo @@ -865,6 +895,8 @@ lib/coq/plugins/micromega/csdpcert.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/csdpcert.cmx lib/coq/plugins/micromega/g_micromega.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/g_micromega.cmx +lib/coq/plugins/micromega/itv.cmi +${PLIST.ocaml-opt}lib/coq/plugins/micromega/itv.cmx lib/coq/plugins/micromega/mfourier.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/mfourier.cmx lib/coq/plugins/micromega/micromega.cmi @@ -879,12 +911,16 @@ lib/coq/plugins/micromega/persistent_cache.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/persistent_cache.cmx lib/coq/plugins/micromega/polynomial.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/polynomial.cmx +lib/coq/plugins/micromega/simplex.cmi +${PLIST.ocaml-opt}lib/coq/plugins/micromega/simplex.cmx lib/coq/plugins/micromega/sos.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/sos.cmx lib/coq/plugins/micromega/sos_lib.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/sos_lib.cmx lib/coq/plugins/micromega/sos_types.cmi ${PLIST.ocaml-opt}lib/coq/plugins/micromega/sos_types.cmx +lib/coq/plugins/micromega/vect.cmi +${PLIST.ocaml-opt}lib/coq/plugins/micromega/vect.cmx lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi ${PLIST.ocaml-opt}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmx ${PLIST.natdynlink}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmxs @@ -940,6 +976,7 @@ lib/coq/plugins/omega/OmegaTactic.vo lib/coq/plugins/omega/PreOmega.glob lib/coq/plugins/omega/PreOmega.v lib/coq/plugins/omega/PreOmega.vo +lib/coq/plugins/omega/coq_omega.cmi ${PLIST.ocaml-opt}lib/coq/plugins/omega/coq_omega.cmx ${PLIST.ocaml-opt}lib/coq/plugins/omega/g_omega.cmx ${PLIST.ocaml-opt}lib/coq/plugins/omega/omega.cmx @@ -947,41 +984,6 @@ lib/coq/plugins/omega/omega_plugin.cmi ${PLIST.ocaml-opt}lib/coq/plugins/omega/omega_plugin.cmx ${PLIST.natdynlink}lib/coq/plugins/omega/omega_plugin.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/omega/omega_plugin.o -lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi -${PLIST.ocaml-opt}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmx -${PLIST.natdynlink}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.o -lib/coq/plugins/quote/Quote.glob -lib/coq/plugins/quote/Quote.v -lib/coq/plugins/quote/Quote.vo -${PLIST.ocaml-opt}lib/coq/plugins/quote/g_quote.cmx -${PLIST.ocaml-opt}lib/coq/plugins/quote/quote.cmx -lib/coq/plugins/quote/quote_plugin.cmi -${PLIST.ocaml-opt}lib/coq/plugins/quote/quote_plugin.cmx -${PLIST.natdynlink}lib/coq/plugins/quote/quote_plugin.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/quote/quote_plugin.o -lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi -${PLIST.ocaml-opt}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmx -${PLIST.natdynlink}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.o -lib/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmi -${PLIST.ocaml-opt}lib/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmx -${PLIST.natdynlink}lib/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.o -lib/coq/plugins/romega/ROmega.glob -lib/coq/plugins/romega/ROmega.v -lib/coq/plugins/romega/ROmega.vo -lib/coq/plugins/romega/ReflOmegaCore.glob -lib/coq/plugins/romega/ReflOmegaCore.v -lib/coq/plugins/romega/ReflOmegaCore.vo -lib/coq/plugins/romega/const_omega.cmi -${PLIST.ocaml-opt}lib/coq/plugins/romega/const_omega.cmx -${PLIST.ocaml-opt}lib/coq/plugins/romega/g_romega.cmx -${PLIST.ocaml-opt}lib/coq/plugins/romega/refl_omega.cmx -lib/coq/plugins/romega/romega_plugin.cmi -${PLIST.ocaml-opt}lib/coq/plugins/romega/romega_plugin.cmx -${PLIST.natdynlink}lib/coq/plugins/romega/romega_plugin.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/romega/romega_plugin.o lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi ${PLIST.ocaml-opt}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx ${PLIST.natdynlink}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmxs @@ -1245,33 +1247,31 @@ lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmi ${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmx ${PLIST.natdynlink}lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/ssrmatching_plugin.o -${PLIST.ocaml-opt}lib/coq/plugins/syntax/ascii_syntax.cmx -lib/coq/plugins/syntax/ascii_syntax_plugin.cmi -${PLIST.ocaml-opt}lib/coq/plugins/syntax/ascii_syntax_plugin.cmx -${PLIST.natdynlink}lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/syntax/ascii_syntax_plugin.o ${PLIST.ocaml-opt}lib/coq/plugins/syntax/g_numeral.cmx -${PLIST.ocaml-opt}lib/coq/plugins/syntax/int31_syntax.cmx -lib/coq/plugins/syntax/int31_syntax_plugin.cmi -${PLIST.ocaml-opt}lib/coq/plugins/syntax/int31_syntax_plugin.cmx -${PLIST.natdynlink}lib/coq/plugins/syntax/int31_syntax_plugin.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/syntax/int31_syntax_plugin.o +${PLIST.ocaml-opt}lib/coq/plugins/syntax/g_string.cmx +${PLIST.ocaml-opt}lib/coq/plugins/syntax/int63_syntax.cmx +lib/coq/plugins/syntax/int63_syntax_plugin.cmi +${PLIST.ocaml-opt}lib/coq/plugins/syntax/int63_syntax_plugin.cmx +${PLIST.ocaml-opt}lib/coq/plugins/syntax/int63_syntax_plugin.cmxs +${PLIST.ocaml-opt}lib/coq/plugins/syntax/int63_syntax_plugin.o lib/coq/plugins/syntax/numeral.cmi ${PLIST.ocaml-opt}lib/coq/plugins/syntax/numeral.cmx lib/coq/plugins/syntax/numeral_notation_plugin.cmi ${PLIST.ocaml-opt}lib/coq/plugins/syntax/numeral_notation_plugin.cmx ${PLIST.natdynlink}lib/coq/plugins/syntax/numeral_notation_plugin.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/syntax/numeral_notation_plugin.o +lib/coq/plugins/syntax/r_syntax.cmi ${PLIST.ocaml-opt}lib/coq/plugins/syntax/r_syntax.cmx lib/coq/plugins/syntax/r_syntax_plugin.cmi ${PLIST.ocaml-opt}lib/coq/plugins/syntax/r_syntax_plugin.cmx ${PLIST.natdynlink}lib/coq/plugins/syntax/r_syntax_plugin.cmxs ${PLIST.ocaml-opt}lib/coq/plugins/syntax/r_syntax_plugin.o -${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_syntax.cmx -lib/coq/plugins/syntax/string_syntax_plugin.cmi -${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_syntax_plugin.cmx -${PLIST.natdynlink}lib/coq/plugins/syntax/string_syntax_plugin.cmxs -${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_syntax_plugin.o +lib/coq/plugins/syntax/string_notation.cmi +${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_notation.cmx +lib/coq/plugins/syntax/string_notation_plugin.cmi +${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_notation_plugin.cmx +${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_notation_plugin.cmxs +${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_notation_plugin.o lib/coq/pretyping/arguments_renaming.cmi ${PLIST.ocaml-opt}lib/coq/pretyping/arguments_renaming.cmx lib/coq/pretyping/cases.cmi @@ -1296,6 +1296,8 @@ lib/coq/pretyping/find_subterm.cmi ${PLIST.ocaml-opt}lib/coq/pretyping/find_subterm.cmx lib/coq/pretyping/geninterp.cmi ${PLIST.ocaml-opt}lib/coq/pretyping/geninterp.cmx +lib/coq/pretyping/globEnv.cmi +${PLIST.ocaml-opt}lib/coq/pretyping/globEnv.cmx lib/coq/pretyping/glob_ops.cmi ${PLIST.ocaml-opt}lib/coq/pretyping/glob_ops.cmx lib/coq/pretyping/glob_term.cmi @@ -1384,12 +1386,8 @@ lib/coq/proofs/proof_bullet.cmi ${PLIST.ocaml-opt}lib/coq/proofs/proof_bullet.cmx lib/coq/proofs/proof_global.cmi ${PLIST.ocaml-opt}lib/coq/proofs/proof_global.cmx -lib/coq/proofs/proof_type.cmi -${PLIST.ocaml-opt}lib/coq/proofs/proof_type.cmx ${PLIST.ocaml-opt}lib/coq/proofs/proofs.a ${PLIST.ocaml-opt}lib/coq/proofs/proofs.cmxa -lib/coq/proofs/redexpr.cmi -${PLIST.ocaml-opt}lib/coq/proofs/redexpr.cmx lib/coq/proofs/refine.cmi ${PLIST.ocaml-opt}lib/coq/proofs/refine.cmx lib/coq/proofs/refiner.cmi @@ -1398,6 +1396,7 @@ lib/coq/proofs/tacmach.cmi ${PLIST.ocaml-opt}lib/coq/proofs/tacmach.cmx lib/coq/proofs/tactypes.cmi ${PLIST.ocaml-opt}lib/coq/proofs/tactypes.cmx +lib/coq/revision lib/coq/stm/asyncTaskQueue.cmi ${PLIST.ocaml-opt}lib/coq/stm/asyncTaskQueue.cmx lib/coq/stm/coqworkmgrApi.cmi @@ -1422,6 +1421,8 @@ lib/coq/stm/vio_checking.cmi ${PLIST.ocaml-opt}lib/coq/stm/vio_checking.cmx lib/coq/stm/workerPool.cmi ${PLIST.ocaml-opt}lib/coq/stm/workerPool.cmx +lib/coq/tactics/abstract.cmi +${PLIST.ocaml-opt}lib/coq/tactics/abstract.cmx lib/coq/tactics/auto.cmi ${PLIST.ocaml-opt}lib/coq/tactics/auto.cmx lib/coq/tactics/autorewrite.cmi @@ -1448,6 +1449,8 @@ lib/coq/tactics/eqschemes.cmi ${PLIST.ocaml-opt}lib/coq/tactics/eqschemes.cmx lib/coq/tactics/equality.cmi ${PLIST.ocaml-opt}lib/coq/tactics/equality.cmx +lib/coq/tactics/genredexpr.cmi +${PLIST.ocaml-opt}lib/coq/tactics/genredexpr.cmx lib/coq/tactics/hints.cmi ${PLIST.ocaml-opt}lib/coq/tactics/hints.cmx lib/coq/tactics/hipattern.cmi @@ -1458,6 +1461,12 @@ lib/coq/tactics/inv.cmi ${PLIST.ocaml-opt}lib/coq/tactics/inv.cmx lib/coq/tactics/leminv.cmi ${PLIST.ocaml-opt}lib/coq/tactics/leminv.cmx +lib/coq/tactics/ppred.cmi +${PLIST.ocaml-opt}lib/coq/tactics/ppred.cmx +lib/coq/tactics/redexpr.cmi +${PLIST.ocaml-opt}lib/coq/tactics/redexpr.cmx +lib/coq/tactics/redops.cmi +${PLIST.ocaml-opt}lib/coq/tactics/redops.cmx lib/coq/tactics/tacticals.cmi ${PLIST.ocaml-opt}lib/coq/tactics/tacticals.cmx ${PLIST.ocaml-opt}lib/coq/tactics/tactics.a @@ -1778,10 +1787,10 @@ lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi ${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx ${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs ${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.o -lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmi -${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmx -${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmxs -${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.o +lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmi +${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmx +${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.o lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmi ${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmx ${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmxs @@ -1793,9 +1802,9 @@ ${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.o lib/coq/theories/Compat/AdmitAxiom.glob lib/coq/theories/Compat/AdmitAxiom.v lib/coq/theories/Compat/AdmitAxiom.vo -lib/coq/theories/Compat/Coq87.glob -lib/coq/theories/Compat/Coq87.v -lib/coq/theories/Compat/Coq87.vo +lib/coq/theories/Compat/Coq810.glob +lib/coq/theories/Compat/Coq810.v +lib/coq/theories/Compat/Coq810.vo lib/coq/theories/Compat/Coq88.glob lib/coq/theories/Compat/Coq88.v lib/coq/theories/Compat/Coq88.vo @@ -1949,6 +1958,10 @@ lib/coq/theories/FSets/FSetWeakList.vo lib/coq/theories/FSets/FSets.glob lib/coq/theories/FSets/FSets.v lib/coq/theories/FSets/FSets.vo +lib/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmi +${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmx +${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Byte.o lib/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmi ${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmx ${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmxs @@ -1997,6 +2010,9 @@ lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmi ${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmx ${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmxs ${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.o +lib/coq/theories/Init/Byte.glob +lib/coq/theories/Init/Byte.v +lib/coq/theories/Init/Byte.vo lib/coq/theories/Init/Datatypes.glob lib/coq/theories/Init/Datatypes.v lib/coq/theories/Init/Datatypes.vo @@ -2221,6 +2237,10 @@ lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmi ${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmx ${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmxs ${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.o +lib/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmi +${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmx +${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.o lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmi ${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmx ${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmxs @@ -2328,6 +2348,9 @@ lib/coq/theories/Logic/SetIsType.vo lib/coq/theories/Logic/SetoidChoice.glob lib/coq/theories/Logic/SetoidChoice.v lib/coq/theories/Logic/SetoidChoice.vo +lib/coq/theories/Logic/StrictProp.glob +lib/coq/theories/Logic/StrictProp.v +lib/coq/theories/Logic/StrictProp.vo lib/coq/theories/Logic/WKL.glob lib/coq/theories/Logic/WKL.v lib/coq/theories/Logic/WKL.vo @@ -2583,6 +2606,27 @@ lib/coq/theories/Numbers/Cyclic/Int31/Int31.vo lib/coq/theories/Numbers/Cyclic/Int31/Ring31.glob lib/coq/theories/Numbers/Cyclic/Int31/Ring31.v lib/coq/theories/Numbers/Cyclic/Int31/Ring31.vo +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmi +${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmx +${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.o +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmi +${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmx +${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.o +lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmi +${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmx +${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.o +lib/coq/theories/Numbers/Cyclic/Int63/Cyclic63.glob +lib/coq/theories/Numbers/Cyclic/Int63/Cyclic63.v +lib/coq/theories/Numbers/Cyclic/Int63/Cyclic63.vo +lib/coq/theories/Numbers/Cyclic/Int63/Int63.glob +lib/coq/theories/Numbers/Cyclic/Int63/Int63.v +lib/coq/theories/Numbers/Cyclic/Int63/Int63.vo +lib/coq/theories/Numbers/Cyclic/Int63/Ring63.glob +lib/coq/theories/Numbers/Cyclic/Int63/Ring63.v +lib/coq/theories/Numbers/Cyclic/Int63/Ring63.vo lib/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmi ${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmx ${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmxs @@ -3437,6 +3481,10 @@ lib/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmi ${PLIST.ocaml-opt}lib/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmx ${PLIST.natdynlink}lib/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmxs ${PLIST.ocaml-opt}lib/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.o +lib/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmi +${PLIST.ocaml-opt}lib/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmx +${PLIST.natdynlink}lib/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.o lib/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmi ${PLIST.ocaml-opt}lib/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmx ${PLIST.natdynlink}lib/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmxs @@ -3628,6 +3676,9 @@ lib/coq/theories/Reals/Rtrigo_fun.vo lib/coq/theories/Reals/Rtrigo_reg.glob lib/coq/theories/Reals/Rtrigo_reg.v lib/coq/theories/Reals/Rtrigo_reg.vo +lib/coq/theories/Reals/Runcountable.glob +lib/coq/theories/Reals/Runcountable.v +lib/coq/theories/Reals/Runcountable.vo lib/coq/theories/Reals/SeqProp.glob lib/coq/theories/Reals/SeqProp.v lib/coq/theories/Reals/SeqProp.vo @@ -3889,6 +3940,14 @@ lib/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmi ${PLIST.ocaml-opt}lib/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmx ${PLIST.natdynlink}lib/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmxs ${PLIST.ocaml-opt}lib/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.o +lib/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmi +${PLIST.ocaml-opt}lib/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmx +${PLIST.natdynlink}lib/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.o +lib/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmi +${PLIST.ocaml-opt}lib/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmx +${PLIST.natdynlink}lib/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmxs +${PLIST.ocaml-opt}lib/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.o lib/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmi ${PLIST.ocaml-opt}lib/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmx ${PLIST.natdynlink}lib/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmxs @@ -3907,6 +3966,12 @@ lib/coq/theories/Strings/Ascii.vo lib/coq/theories/Strings/BinaryString.glob lib/coq/theories/Strings/BinaryString.v lib/coq/theories/Strings/BinaryString.vo +lib/coq/theories/Strings/Byte.glob +lib/coq/theories/Strings/Byte.v +lib/coq/theories/Strings/Byte.vo +lib/coq/theories/Strings/ByteVector.glob +lib/coq/theories/Strings/ByteVector.v +lib/coq/theories/Strings/ByteVector.vo lib/coq/theories/Strings/HexString.glob lib/coq/theories/Strings/HexString.v lib/coq/theories/Strings/HexString.vo @@ -4364,12 +4429,19 @@ lib/coq/tools/coqdoc/coqdoc.sty lib/coq/tools/make-both-single-timing-files.py lib/coq/tools/make-both-time-files.py lib/coq/tools/make-one-time-file.py +${PLIST.ocaml-opt}lib/coq/topbin/coqc_bin.cmx ${PLIST.ocaml-opt}lib/coq/topbin/coqproofworker_bin.cmx ${PLIST.ocaml-opt}lib/coq/topbin/coqqueryworker_bin.cmx ${PLIST.ocaml-opt}lib/coq/topbin/coqtacticworker_bin.cmx ${PLIST.ocaml-opt}lib/coq/topbin/coqtop_bin.cmx +lib/coq/toplevel/ccompile.cmi +${PLIST.ocaml-opt}lib/coq/toplevel/ccompile.cmx lib/coq/toplevel/coqargs.cmi ${PLIST.ocaml-opt}lib/coq/toplevel/coqargs.cmx +lib/coq/toplevel/coqc.cmi +${PLIST.ocaml-opt}lib/coq/toplevel/coqc.cmx +lib/coq/toplevel/coqcargs.cmi +${PLIST.ocaml-opt}lib/coq/toplevel/coqcargs.cmx lib/coq/toplevel/coqinit.cmi ${PLIST.ocaml-opt}lib/coq/toplevel/coqinit.cmx lib/coq/toplevel/coqloop.cmi @@ -4388,6 +4460,8 @@ lib/coq/toplevel/workerLoop.cmi ${PLIST.ocaml-opt}lib/coq/toplevel/workerLoop.cmx lib/coq/vernac/assumptions.cmi ${PLIST.ocaml-opt}lib/coq/vernac/assumptions.cmx +lib/coq/vernac/attributes.cmi +${PLIST.ocaml-opt}lib/coq/vernac/attributes.cmx lib/coq/vernac/auto_ind_decl.cmi ${PLIST.ocaml-opt}lib/coq/vernac/auto_ind_decl.cmx lib/coq/vernac/class.cmi @@ -4426,8 +4500,6 @@ lib/coq/vernac/locality.cmi ${PLIST.ocaml-opt}lib/coq/vernac/locality.cmx lib/coq/vernac/metasyntax.cmi ${PLIST.ocaml-opt}lib/coq/vernac/metasyntax.cmx -lib/coq/vernac/misctypes.cmi -${PLIST.ocaml-opt}lib/coq/vernac/misctypes.cmx lib/coq/vernac/mltop.cmi ${PLIST.ocaml-opt}lib/coq/vernac/mltop.cmx lib/coq/vernac/obligations.cmi @@ -4450,8 +4522,8 @@ lib/coq/vernac/vernacentries.cmi ${PLIST.ocaml-opt}lib/coq/vernac/vernacentries.cmx lib/coq/vernac/vernacexpr.cmi ${PLIST.ocaml-opt}lib/coq/vernac/vernacexpr.cmx -lib/coq/vernac/vernacinterp.cmi -${PLIST.ocaml-opt}lib/coq/vernac/vernacinterp.cmx +lib/coq/vernac/vernacextend.cmi +${PLIST.ocaml-opt}lib/coq/vernac/vernacextend.cmx lib/coq/vernac/vernacprop.cmi ${PLIST.ocaml-opt}lib/coq/vernac/vernacprop.cmx lib/coq/vernac/vernacstate.cmi @@ -4471,6 +4543,7 @@ share/coq/coq-ssreflect.lang share/coq/coq.lang share/coq/coq.png share/coq/coq_style.xml +share/coq/default.bindings ${PLIST.coqide}share/doc/coq/FAQ-CoqIde ${PLIST.doc}share/doc/coq/LICENSE.doc ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Arith.html diff --git a/lang/coq/distinfo b/lang/coq/distinfo index b6fb157ce0d..419956523a2 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,8 +1,7 @@ -$NetBSD: distinfo,v 1.34 2019/09/01 00:51:46 markd Exp $ +$NetBSD: distinfo,v 1.35 2020/01/24 15:54:48 jaapb Exp $ -SHA1 (coq-8.9.1.tar.gz) = d26646b33922bcd9eb44ef80162f8d0513784e46 -RMD160 (coq-8.9.1.tar.gz) = d82a0f7d31c0e5d7b8b566cd15d7ff9f724c250b -SHA512 (coq-8.9.1.tar.gz) = 66344f801b955d1b6daf3ab1d704551070c95cf9032ae74f15fb33f7ec313812b3e05c0ec277a2eb448e3fdfd9721df06d36612e2fb4928b6530d70147f1d983 -Size (coq-8.9.1.tar.gz) = 6001970 bytes -SHA1 (patch-Makefile.build) = 0438c2f4084dcb411bf8fdb0e513b5769d6419a7 -SHA1 (patch-Makefile.common) = f232485fddc61c51cd12ac5567b706f5f2299328 +SHA1 (coq-8.10.2.tar.gz) = ecdb79a8b4cd76912b39e037ef52545406e63799 +RMD160 (coq-8.10.2.tar.gz) = a3686508b97a98b668c91a513e73f88dff02af89 +SHA512 (coq-8.10.2.tar.gz) = 80df91b64efc9907480388ec479362ee21067c64436da720989d6d1645ffc2f2230ae5c13069c55842da3baa7facbd143c2190d1d64d8c87935802000a02156f +Size (coq-8.10.2.tar.gz) = 6222940 bytes +SHA1 (patch-Makefile.common) = 85bcb271103f87f1e1573d3856740319ee0344cd diff --git a/lang/coq/options.mk b/lang/coq/options.mk index 477b0d2276f..103240f2a0a 100644 --- a/lang/coq/options.mk +++ b/lang/coq/options.mk @@ -1,4 +1,4 @@ -# $NetBSD: options.mk,v 1.8 2019/11/03 19:03:57 rillig Exp $ +# $NetBSD: options.mk,v 1.9 2020/01/24 15:54:48 jaapb Exp $ PKG_OPTIONS_VAR= PKG_OPTIONS.coq PKG_SUPPORTED_OPTIONS= doc coqide @@ -51,8 +51,9 @@ CONFIGURE_ARGS+= -with-doc no .endif .if !empty(PKG_OPTIONS:Mcoqide) -.include "../../x11/ocaml-lablgtk/buildlink3.mk" -.include "../../x11/gtk2/buildlink3.mk" +.include "../../x11/ocaml-lablgtk3/buildlink3.mk" +.include "../../x11/gtk3/buildlink3.mk" +CONFIGURE_ARGS+= -coqide ${COQIDE_TYPE} PLIST.coqide= yes .else CONFIGURE_ARGS+= -coqide no diff --git a/lang/coq/patches/patch-Makefile.build b/lang/coq/patches/patch-Makefile.build deleted file mode 100644 index 6b8ac17a405..00000000000 --- a/lang/coq/patches/patch-Makefile.build +++ /dev/null @@ -1,15 +0,0 @@ -$NetBSD: patch-Makefile.build,v 1.5 2019/09/01 00:51:47 markd Exp $ - -ocaml 4.08 patch - ---- Makefile.build.orig 2019-05-17 12:19:23.000000000 +0000 -+++ Makefile.build -@@ -262,7 +262,7 @@ endef - CAMLP5DEPS:=grammar/grammar.cma - CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) - --PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) -+PR_O := $(if $(READABLE_ML4),pr_o.cmo,) - - # Main packages linked by Coq. - SYSMOD:=-package num,str,unix,dynlink,threads diff --git a/lang/coq/patches/patch-Makefile.common b/lang/coq/patches/patch-Makefile.common index fb60da1f81a..d92820f9b1e 100644 --- a/lang/coq/patches/patch-Makefile.common +++ b/lang/coq/patches/patch-Makefile.common @@ -1,6 +1,7 @@ -$NetBSD: patch-Makefile.common,v 1.5 2019/03/06 09:28:23 jaapb Exp $ +$NetBSD: patch-Makefile.common,v 1.6 2020/01/24 15:54:48 jaapb Exp $ Use BSD_INSTALL_* + --- Makefile.common.orig 2018-10-31 12:53:51.000000000 +0000 +++ Makefile.common @@ -83,8 +83,8 @@ DYNOBJ:=.cmo |