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.

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