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: Fri Jan 24 15:54:49 UTC 2020
Modified Files:
pkgsrc/lang/coq: Makefile PLIST distinfo options.mk
pkgsrc/lang/coq/patches: patch-Makefile.common
Removed Files:
pkgsrc/lang/coq/patches: patch-Makefile.build
Log Message:
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.
To generate a diff of this commit:
cvs rdiff -u -r1.127 -r1.128 pkgsrc/lang/coq/Makefile
cvs rdiff -u -r1.29 -r1.30 pkgsrc/lang/coq/PLIST
cvs rdiff -u -r1.34 -r1.35 pkgsrc/lang/coq/distinfo
cvs rdiff -u -r1.8 -r1.9 pkgsrc/lang/coq/options.mk
cvs rdiff -u -r1.5 -r0 pkgsrc/lang/coq/patches/patch-Makefile.build
cvs rdiff -u -r1.5 -r1.6 pkgsrc/lang/coq/patches/patch-Makefile.common
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Modified files:
Index: pkgsrc/lang/coq/Makefile
diff -u pkgsrc/lang/coq/Makefile:1.127 pkgsrc/lang/coq/Makefile:1.128
--- pkgsrc/lang/coq/Makefile:1.127 Sat Jan 18 21:49:42 2020
+++ pkgsrc/lang/coq/Makefile Fri Jan 24 15:54:48 2020
@@ -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@localhost
-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}/${PKG
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.1
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 buildlin
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"
Index: pkgsrc/lang/coq/PLIST
diff -u pkgsrc/lang/coq/PLIST:1.29 pkgsrc/lang/coq/PLIST:1.30
--- pkgsrc/lang/coq/PLIST:1.29 Wed Mar 6 09:28:23 2019
+++ pkgsrc/lang/coq/PLIST Fri Jan 24 15:54:48 2020
@@ -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.c
${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
${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/N
${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/ExtrHaskellZI
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/NC
${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_cac
${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_
${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
${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/Compa
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_I
${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_
${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/In
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_
${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/NCo
${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
Index: pkgsrc/lang/coq/distinfo
diff -u pkgsrc/lang/coq/distinfo:1.34 pkgsrc/lang/coq/distinfo:1.35
--- pkgsrc/lang/coq/distinfo:1.34 Sun Sep 1 00:51:46 2019
+++ pkgsrc/lang/coq/distinfo Fri Jan 24 15:54:48 2020
@@ -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
Index: pkgsrc/lang/coq/options.mk
diff -u pkgsrc/lang/coq/options.mk:1.8 pkgsrc/lang/coq/options.mk:1.9
--- pkgsrc/lang/coq/options.mk:1.8 Sun Nov 3 19:03:57 2019
+++ pkgsrc/lang/coq/options.mk Fri Jan 24 15:54:48 2020
@@ -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
Index: pkgsrc/lang/coq/patches/patch-Makefile.common
diff -u pkgsrc/lang/coq/patches/patch-Makefile.common:1.5 pkgsrc/lang/coq/patches/patch-Makefile.common:1.6
--- pkgsrc/lang/coq/patches/patch-Makefile.common:1.5 Wed Mar 6 09:28:23 2019
+++ pkgsrc/lang/coq/patches/patch-Makefile.common Fri Jan 24 15:54:48 2020
@@ -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
Home |
Main Index |
Thread Index |
Old Index