Updated lang/coq to version 8.7.0.

Includes many improvements and bugfixes (none that seem to be breaking
backwards compatibility though), see the CHANGELOG.
For packaging:
- camlp4 support removed, package now uses camlp5 exclusively
- fix for PR pkg/52651

5 files changed, 233 insertions, 357 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index f9976a49fc1..7f1950f9894 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.100 2017/09/18 09:53:24 maya Exp $
+# $NetBSD: Makefile,v 1.101 2017/11/03 11:20:28 jaapb Exp $
 #
 
-DISTNAME=	coq-8.6.1
-PKGREVISION=	1
+DISTNAME=	coq-8.7.0
 CATEGORIES=	lang math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -19,7 +18,6 @@ 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
-BUILD_TARGET=		world
 
 BUILDLINK_API_DEPENDS.ocaml+=	ocaml>=3.10
 
@@ -32,9 +30,12 @@ PLIST_SUBST+=	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"
 CONFIGURE_ARGS+=	-native-compiler no
+BUILD_TARGET=	byte
+INSTALL_TARGET=	install-byte
 .endif
 
 .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
@@ -47,7 +48,17 @@ PLIST.natdynlink=	yes
 .  endif
 .endif
 
+.include "../../lang/python/pyversion.mk"
+
 REPLACE_SH=	configure install.sh
+REPLACE_INTERPRETER+=	python
+REPLACE.python.old=	python
+REPLACE.python.new=	${PYTHONBIN}
+REPLACE_FILES.python=	tools/TimeFileMaker.py \
+	tools/make-both-single-timing-files.py \
+	tools/make-both-time-files.py \
+	tools/make-one-time-file.py
+
 INSTALL_ENV+=	COQINSTALLPREFIX=${DESTDIR}
 
 PLIST_VARS+=		coqide natdynlink doc
@@ -63,6 +74,7 @@ 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/camlp4/buildlink3.mk"
+
+.include "../../lang/camlp5/buildlink3.mk"
 .include "../../mk/pthread.buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff --git a/lang/coq/PLIST b/lang/coq/PLIST
index 64805eec97b..5c781039226 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.21 2017/09/08 17:19:01 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.22 2017/11/03 11:20:28 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -8,14 +8,13 @@ bin/coqdoc
 ${PLIST.coqide}bin/coqide
 bin/coqmktop
 bin/coqtop
-bin/coqtop.byte
 bin/coqwc
 bin/coqworkmgr
 bin/gallina
 lib/coq/META
-lib/coq/dllcoqrun.so
+lib/coq/config/coq_config.cmi
+lib/coq/engine/eConstr.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/engine.a
-lib/coq/engine/engine.cma
 ${PLIST.ocaml-opt}lib/coq/engine/engine.cmxa
 lib/coq/engine/evarutil.cmi
 lib/coq/engine/evd.cmi
@@ -25,13 +24,12 @@ lib/coq/engine/logic_monad.cmi
 lib/coq/engine/namegen.cmi
 lib/coq/engine/proofview.cmi
 lib/coq/engine/proofview_monad.cmi
-lib/coq/engine/sigma.cmi
 lib/coq/engine/termops.cmi
 lib/coq/engine/uState.cmi
+lib/coq/engine/universes.cmi
 lib/coq/config/coq_config.cmi
 lib/coq/grammar/grammar.cma
 lib/coq/grammar/q_util.cmi
-lib/coq/grammar/compat5.cmo
 ${PLIST.coqide}lib/coq/ide/config_lexer.cmi
 ${PLIST.coqide}lib/coq/ide/coq.cmi
 ${PLIST.coqide}lib/coq/ide/coqOps.cmi
@@ -42,28 +40,21 @@ ${PLIST.coqide}lib/coq/ide/coqide_ui.cmi
 ${PLIST.coqide}lib/coq/ide/document.cmi
 ${PLIST.coqide}lib/coq/ide/fileOps.cmi
 ${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi
-${PLIST.coqide}lib/coq/ide/ide.a
-${PLIST.coqide}lib/coq/ide/ide.cma
-${PLIST.coqide}lib/coq/ide/ide.cmxa
+${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/minilib.cmi
 ${PLIST.coqide}lib/coq/ide/nanoPG.cmi
 ${PLIST.coqide}lib/coq/ide/preferences.cmi
-${PLIST.coqide}lib/coq/ide/project_file.cmi
-${PLIST.coqide}lib/coq/ide/richprinter.cmi
+${PLIST.coqide}lib/coq/ide/richpp.cmi
 ${PLIST.coqide}lib/coq/ide/sentence.cmi
-${PLIST.coqide}lib/coq/ide/session.cmi
 ${PLIST.coqide}lib/coq/ide/serialize.cmi
+${PLIST.coqide}lib/coq/ide/session.cmi
 ${PLIST.coqide}lib/coq/ide/tags.cmi
 ${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
-${PLIST.coqide}lib/coq/ide/utils/config_file.cmi
 ${PLIST.coqide}lib/coq/ide/utils/configwin.cmi
 ${PLIST.coqide}lib/coq/ide/utils/configwin_ihm.cmi
-${PLIST.coqide}lib/coq/ide/utils/configwin_keys.cmi
 ${PLIST.coqide}lib/coq/ide/utils/configwin_messages.cmi
-${PLIST.coqide}lib/coq/ide/utils/configwin_types.cmi
-${PLIST.coqide}lib/coq/ide/utils/editable_cells.cmi
-${PLIST.coqide}lib/coq/ide/utils/okey.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Command.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Completion.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Detachable.cmi
@@ -73,21 +64,20 @@ ${PLIST.coqide}lib/coq/ide/wg_Notebook.cmi
 ${PLIST.coqide}lib/coq/ide/wg_ProofView.cmi
 ${PLIST.coqide}lib/coq/ide/wg_ScriptView.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Segment.cmi
-${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
 ${PLIST.coqide}lib/coq/ide/xml_lexer.cmi
 ${PLIST.coqide}lib/coq/ide/xml_parser.cmi
 ${PLIST.coqide}lib/coq/ide/xml_printer.cmi
-lib/coq/interp/constrarg.cmi
+${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
 lib/coq/interp/constrexpr_ops.cmi
 lib/coq/interp/constrextern.cmi
 lib/coq/interp/constrintern.cmi
-lib/coq/interp/coqlib.cmi
+lib/coq/interp/declare.cmi
 lib/coq/interp/dumpglob.cmi
 lib/coq/interp/genintern.cmi
+lib/coq/interp/impargs.cmi
 lib/coq/interp/implicit_quantifiers.cmi
-lib/coq/interp/interp.a
-lib/coq/interp/interp.cma
-lib/coq/interp/interp.cmxa
+${PLIST.ocaml-opt}lib/coq/interp/interp.a
+${PLIST.ocaml-opt}lib/coq/interp/interp.cmxa
 lib/coq/interp/modintern.cmi
 lib/coq/interp/notation.cmi
 lib/coq/interp/notation_ops.cmi
@@ -103,12 +93,16 @@ lib/coq/intf/evar_kinds.cmi
 lib/coq/intf/extend.cmi
 lib/coq/intf/genredexpr.cmi
 lib/coq/intf/glob_term.cmi
+${PLIST.ocaml-opt}lib/coq/intf/intf.a
+${PLIST.ocaml-opt}lib/coq/intf/intf.cmxa
 lib/coq/intf/locus.cmi
 lib/coq/intf/misctypes.cmi
 lib/coq/intf/notation_term.cmi
 lib/coq/intf/pattern.cmi
-lib/coq/intf/tacexpr.cmi
+lib/coq/intf/tactypes.cmi
 lib/coq/intf/vernacexpr.cmi
+lib/coq/kernel/byterun/dllcoqrun.so
+lib/coq/kernel/byterun/libcoqrun.a
 lib/coq/kernel/cClosure.cmi
 lib/coq/kernel/cbytecodes.cmi
 lib/coq/kernel/cbytegen.cmi
@@ -125,12 +119,10 @@ lib/coq/kernel/entries.cmi
 lib/coq/kernel/environ.cmi
 lib/coq/kernel/esubst.cmi
 lib/coq/kernel/evar.cmi
-lib/coq/kernel/fast_typeops.cmi
 lib/coq/kernel/indtypes.cmi
 lib/coq/kernel/inductive.cmi
-lib/coq/kernel/kernel.a
-lib/coq/kernel/kernel.cma
-lib/coq/kernel/kernel.cmxa
+${PLIST.ocaml-opt}lib/coq/kernel/kernel.a
+${PLIST.ocaml-opt}lib/coq/kernel/kernel.cmxa
 lib/coq/kernel/mod_subst.cmi
 lib/coq/kernel/mod_typing.cmi
 lib/coq/kernel/modops.cmi
@@ -164,6 +156,7 @@ lib/coq/lib/aux_file.cmi
 lib/coq/lib/backtrace.cmi
 lib/coq/lib/bigint.cmi
 lib/coq/lib/cArray.cmi
+lib/coq/lib/cAst.cmi
 lib/coq/lib/cEphemeron.cmi
 lib/coq/lib/cErrors.cmi
 lib/coq/lib/cList.cmi
@@ -177,10 +170,10 @@ lib/coq/lib/cThread.cmi
 lib/coq/lib/cUnix.cmi
 lib/coq/lib/cWarnings.cmi
 lib/coq/lib/canary.cmi
-lib/coq/lib/clib.a
-lib/coq/lib/clib.cma
-lib/coq/lib/clib.cmxa
+${PLIST.ocaml-opt}lib/coq/lib/clib.a
+${PLIST.ocaml-opt}lib/coq/lib/clib.cmxa
 lib/coq/lib/control.cmi
+lib/coq/lib/coqProject_file.cmi
 lib/coq/lib/deque.cmi
 lib/coq/lib/dyn.cmi
 lib/coq/lib/envars.cmi
@@ -197,20 +190,16 @@ lib/coq/lib/heap.cmi
 lib/coq/lib/hook.cmi
 lib/coq/lib/iStream.cmi
 lib/coq/lib/int.cmi
-lib/coq/lib/lib.a
-lib/coq/lib/lib.cma
-lib/coq/lib/lib.cmxa
+${PLIST.ocaml-opt}lib/coq/lib/lib.a
+${PLIST.ocaml-opt}lib/coq/lib/lib.cmxa
 lib/coq/lib/loc.cmi
 lib/coq/lib/minisys.cmi
 lib/coq/lib/monad.cmi
 lib/coq/lib/option.cmi
 lib/coq/lib/pp.cmi
-lib/coq/lib/pp_control.cmi
-lib/coq/lib/ppstyle.cmi
 lib/coq/lib/predicate.cmi
 lib/coq/lib/profile.cmi
 lib/coq/lib/remoteCounter.cmi
-lib/coq/lib/richpp.cmi
 lib/coq/lib/rtree.cmi
 lib/coq/lib/segmenttree.cmi
 lib/coq/lib/spawn.cmi
@@ -224,8 +213,7 @@ lib/coq/lib/unicodetable.cmi
 lib/coq/lib/unionfind.cmi
 lib/coq/lib/util.cmi
 lib/coq/lib/xml_datatype.cmi
-lib/coq/libcoqrun.a
-lib/coq/library/declare.cmi
+lib/coq/library/coqlib.cmi
 lib/coq/library/declaremods.cmi
 lib/coq/library/decls.cmi
 lib/coq/library/dischargedhypsmap.cmi
@@ -233,62 +221,31 @@ lib/coq/library/global.cmi
 lib/coq/library/globnames.cmi
 lib/coq/library/goptions.cmi
 lib/coq/library/heads.cmi
-lib/coq/library/impargs.cmi
 lib/coq/library/keys.cmi
 lib/coq/library/kindops.cmi
 lib/coq/library/lib.cmi
 lib/coq/library/libnames.cmi
 lib/coq/library/libobject.cmi
-lib/coq/library/library.a
-lib/coq/library/library.cma
+${PLIST.ocaml-opt}lib/coq/library/library.a
 lib/coq/library/library.cmi
-lib/coq/library/library.cmxa
+${PLIST.ocaml-opt}lib/coq/library/library.cmxa
 lib/coq/library/loadpath.cmi
 lib/coq/library/nameops.cmi
 lib/coq/library/nametab.cmi
 lib/coq/library/states.cmi
 lib/coq/library/summary.cmi
-lib/coq/library/universes.cmi
-lib/coq/ltac/coretactics.cmi
-lib/coq/ltac/evar_tactics.cmi
-lib/coq/ltac/extraargs.cmi
-lib/coq/ltac/extratactics.cmi
-lib/coq/ltac/g_auto.cmi
-lib/coq/ltac/g_class.cmi
-lib/coq/ltac/g_eqdecide.cmi
-lib/coq/ltac/g_ltac.cmi
-lib/coq/ltac/g_obligations.cmi
-lib/coq/ltac/g_rewrite.cmi
-${PLIST.ocaml-opt}lib/coq/ltac/ltac.a
-lib/coq/ltac/ltac.cma
-${PLIST.ocaml-opt}lib/coq/ltac/ltac.cmxa
-lib/coq/ltac/profile_ltac.cmi
-lib/coq/ltac/profile_ltac_tactics.cmi
-lib/coq/ltac/rewrite.cmi
-lib/coq/ltac/taccoerce.cmi
-lib/coq/ltac/tacentries.cmi
-lib/coq/ltac/tacenv.cmi
-lib/coq/ltac/tacintern.cmi
-lib/coq/ltac/tacinterp.cmi
-lib/coq/ltac/tacsubst.cmi
-lib/coq/ltac/tactic_debug.cmi
-lib/coq/ltac/tactic_option.cmi
-lib/coq/ltac/tauto.cmi
+lib/coq/library/univops.cmi
 lib/coq/parsing/cLexer.cmi
-lib/coq/parsing/compat.cmi
 lib/coq/parsing/egramcoq.cmi
 lib/coq/parsing/egramml.cmi
 lib/coq/parsing/g_constr.cmi
 lib/coq/parsing/g_prim.cmi
 lib/coq/parsing/g_proofs.cmi
-lib/coq/parsing/g_tactic.cmi
 lib/coq/parsing/g_vernac.cmi
-lib/coq/parsing/highparsing.a
-lib/coq/parsing/highparsing.cma
-lib/coq/parsing/highparsing.cmxa
-lib/coq/parsing/parsing.a
-lib/coq/parsing/parsing.cma
-lib/coq/parsing/parsing.cmxa
+${PLIST.ocaml-opt}lib/coq/parsing/highparsing.a
+${PLIST.ocaml-opt}lib/coq/parsing/highparsing.cmxa
+${PLIST.ocaml-opt}lib/coq/parsing/parsing.a
+${PLIST.ocaml-opt}lib/coq/parsing/parsing.cmxa
 lib/coq/parsing/pcoq.cmi
 lib/coq/parsing/tok.cmi
 ${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
@@ -313,32 +270,21 @@ lib/coq/plugins/btauto/Reflect.glob
 lib/coq/plugins/btauto/Reflect.v
 lib/coq/plugins/btauto/Reflect.vo
 lib/coq/plugins/btauto/btauto_plugin.cmi
-lib/coq/plugins/btauto/btauto_plugin.cmo
-lib/coq/plugins/btauto/btauto_plugin.cmxs
+${PLIST.natdynlink}lib/coq/plugins/btauto/btauto_plugin.cmxs
 lib/coq/plugins/cc/cc_plugin.cmi
-lib/coq/plugins/cc/cc_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/cc/cc_plugin.cmxs
 lib/coq/plugins/cc/ccalgo.cmi
 lib/coq/plugins/cc/ccproof.cmi
 lib/coq/plugins/cc/cctac.cmi
-lib/coq/plugins/decl_mode/decl_expr.cmi
-lib/coq/plugins/decl_mode/decl_interp.cmi
-lib/coq/plugins/decl_mode/decl_mode.cmi
-lib/coq/plugins/decl_mode/decl_mode_plugin.cmi
-lib/coq/plugins/decl_mode/decl_mode_plugin.cmo
-${PLIST.natdynlink}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
-lib/coq/plugins/decl_mode/decl_proof_instr.cmi
-lib/coq/plugins/decl_mode/ppdecl_proof.cmi
 lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmx
-lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmxs
+${PLIST.natdynlink}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.o
 lib/coq/plugins/derive/Derive.glob
 lib/coq/plugins/derive/Derive.v
 lib/coq/plugins/derive/Derive.vo
 lib/coq/plugins/derive/derive.cmi
 lib/coq/plugins/derive/derive_plugin.cmi
-lib/coq/plugins/derive/derive_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/derive/derive_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmx
@@ -463,7 +409,6 @@ lib/coq/plugins/extraction/common.cmi
 lib/coq/plugins/extraction/extract_env.cmi
 lib/coq/plugins/extraction/extraction.cmi
 lib/coq/plugins/extraction/extraction_plugin.cmi
-lib/coq/plugins/extraction/extraction_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/extraction/extraction_plugin.cmxs
 lib/coq/plugins/extraction/haskell.cmi
 lib/coq/plugins/extraction/json.cmi
@@ -476,7 +421,6 @@ lib/coq/plugins/extraction/table.cmi
 lib/coq/plugins/firstorder/formula.cmi
 lib/coq/plugins/firstorder/ground.cmi
 lib/coq/plugins/firstorder/ground_plugin.cmi
-lib/coq/plugins/firstorder/ground_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/firstorder/ground_plugin.cmxs
 lib/coq/plugins/firstorder/instances.cmi
 lib/coq/plugins/firstorder/rules.cmi
@@ -497,7 +441,6 @@ lib/coq/plugins/fourier/Fourier_util.glob
 lib/coq/plugins/fourier/Fourier_util.v
 lib/coq/plugins/fourier/Fourier_util.vo
 lib/coq/plugins/fourier/fourier_plugin.cmi
-lib/coq/plugins/fourier/fourier_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/fourier/fourier_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmx
@@ -521,23 +464,41 @@ lib/coq/plugins/funind/indfun.cmi
 lib/coq/plugins/funind/indfun_common.cmi
 lib/coq/plugins/funind/recdef.cmi
 lib/coq/plugins/funind/recdef_plugin.cmi
-lib/coq/plugins/funind/recdef_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/funind/recdef_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.o
-${PLIST.native}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.o
-lib/coq/plugins/ltac/LtacDummy.glob
-lib/coq/plugins/ltac/LtacDummy.v
-lib/coq/plugins/ltac/LtacDummy.vo
-lib/coq/plugins/ltac/ltac_dummy.cmi
 lib/coq/plugins/ltac/ltac_plugin.cmi
-lib/coq/plugins/ltac/ltac_plugin.cmo
-lib/coq/plugins/ltac/ltac_plugin.cmxs
+${PLIST.natdynlink}lib/coq/plugins/ltac/ltac_plugin.cmxs
+${PLIST.native}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.o
+lib/coq/plugins/ltac/Ltac.glob
+lib/coq/plugins/ltac/Ltac.v
+lib/coq/plugins/ltac/Ltac.vo
+lib/coq/plugins/ltac/evar_tactics.cmi
+lib/coq/plugins/ltac/extraargs.cmi
+lib/coq/plugins/ltac/extratactics.cmi
+lib/coq/plugins/ltac/pltac.cmi
+lib/coq/plugins/ltac/pptactic.cmi
+lib/coq/plugins/ltac/profile_ltac.cmi
+lib/coq/plugins/ltac/rewrite.cmi
+lib/coq/plugins/ltac/tacarg.cmi
+lib/coq/plugins/ltac/taccoerce.cmi
+lib/coq/plugins/ltac/tacentries.cmi
+lib/coq/plugins/ltac/tacenv.cmi
+lib/coq/plugins/ltac/tacexpr.cmi
+lib/coq/plugins/ltac/tacintern.cmi
+lib/coq/plugins/ltac/tacinterp.cmi
+lib/coq/plugins/ltac/tacsubst.cmi
+lib/coq/plugins/ltac/tactic_debug.cmi
+lib/coq/plugins/ltac/tactic_matching.cmi
+lib/coq/plugins/ltac/tactic_option.cmi
+lib/coq/plugins/ltac/tauto.cmi
+lib/coq/plugins/ltac/tauto_plugin.cmi
+${PLIST.natdynlink}lib/coq/plugins/ltac/tauto_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmxs
@@ -554,6 +515,10 @@ ${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.o
+${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.o
 ${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmxs
@@ -609,6 +574,9 @@ lib/coq/plugins/micromega/Lqa.vo
 lib/coq/plugins/micromega/Lra.glob
 lib/coq/plugins/micromega/Lra.v
 lib/coq/plugins/micromega/Lra.vo
+lib/coq/plugins/micromega/MExtraction.glob
+lib/coq/plugins/micromega/MExtraction.v
+lib/coq/plugins/micromega/MExtraction.vo
 lib/coq/plugins/micromega/OrderedRing.glob
 lib/coq/plugins/micromega/OrderedRing.v
 lib/coq/plugins/micromega/OrderedRing.vo
@@ -642,9 +610,9 @@ lib/coq/plugins/micromega/ZMicromega.vo
 lib/coq/plugins/micromega/csdpcert
 lib/coq/plugins/micromega/micromega.cmi
 lib/coq/plugins/micromega/micromega_plugin.cmi
-lib/coq/plugins/micromega/micromega_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/micromega/micromega_plugin.cmxs
 lib/coq/plugins/micromega/sos.cmi
+lib/coq/plugins/micromega/sos_types.cmi
 ${PLIST.native}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmxs
@@ -655,7 +623,6 @@ lib/coq/plugins/nsatz/Nsatz.vo
 lib/coq/plugins/nsatz/ideal.cmi
 lib/coq/plugins/nsatz/nsatz.cmi
 lib/coq/plugins/nsatz/nsatz_plugin.cmi
-lib/coq/plugins/nsatz/nsatz_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/nsatz/nsatz_plugin.cmxs
 lib/coq/plugins/nsatz/polynom.cmi
 lib/coq/plugins/nsatz/utile.cmi
@@ -695,7 +662,6 @@ lib/coq/plugins/omega/PreOmega.glob
 lib/coq/plugins/omega/PreOmega.v
 lib/coq/plugins/omega/PreOmega.vo
 lib/coq/plugins/omega/omega_plugin.cmi
-lib/coq/plugins/omega/omega_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/omega/omega_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmx
@@ -705,7 +671,6 @@ lib/coq/plugins/quote/Quote.glob
 lib/coq/plugins/quote/Quote.v
 lib/coq/plugins/quote/Quote.vo
 lib/coq/plugins/quote/quote_plugin.cmi
-lib/coq/plugins/quote/quote_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/quote/quote_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmx
@@ -723,7 +688,6 @@ lib/coq/plugins/romega/ReflOmegaCore.v
 lib/coq/plugins/romega/ReflOmegaCore.vo
 lib/coq/plugins/romega/const_omega.cmi
 lib/coq/plugins/romega/romega_plugin.cmi
-lib/coq/plugins/romega/romega_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/romega/romega_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx
@@ -742,7 +706,6 @@ lib/coq/plugins/rtauto/Rtauto.vo
 lib/coq/plugins/rtauto/proof_search.cmi
 lib/coq/plugins/rtauto/refl_tauto.cmi
 lib/coq/plugins/rtauto/rtauto_plugin.cmi
-lib/coq/plugins/rtauto/rtauto_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/rtauto/rtauto_plugin.cmxs
 ${PLIST.native}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmx
@@ -915,8 +878,42 @@ lib/coq/plugins/setoid_ring/ZArithRing.vo
 lib/coq/plugins/setoid_ring/newring.cmi
 lib/coq/plugins/setoid_ring/newring_ast.cmi
 lib/coq/plugins/setoid_ring/newring_plugin.cmi
-lib/coq/plugins/setoid_ring/newring_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/setoid_ring/newring_plugin.cmxs
+${PLIST.native}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.o
+${PLIST.native}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.o
+${PLIST.native}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.o
+lib/coq/plugins/ssr/ssrast.cmi
+lib/coq/plugins/ssr/ssrbool.glob
+lib/coq/plugins/ssr/ssrbool.v
+lib/coq/plugins/ssr/ssrbool.vo
+lib/coq/plugins/ssr/ssrbwd.cmi
+lib/coq/plugins/ssr/ssrcommon.cmi
+lib/coq/plugins/ssr/ssreflect.glob
+lib/coq/plugins/ssr/ssreflect.v
+lib/coq/plugins/ssr/ssreflect.vo
+lib/coq/plugins/ssr/ssreflect_plugin.cmi
+lib/coq/plugins/ssr/ssreflect_plugin.cmxs
+lib/coq/plugins/ssr/ssrelim.cmi
+lib/coq/plugins/ssr/ssrequality.cmi
+lib/coq/plugins/ssr/ssrfun.glob
+lib/coq/plugins/ssr/ssrfun.v
+lib/coq/plugins/ssr/ssrfun.vo
+lib/coq/plugins/ssr/ssrfwd.cmi
+lib/coq/plugins/ssr/ssripats.cmi
+lib/coq/plugins/ssr/ssrparser.cmi
+lib/coq/plugins/ssr/ssrprinters.cmi
+lib/coq/plugins/ssr/ssrtacticals.cmi
+lib/coq/plugins/ssr/ssrvernac.cmi
+lib/coq/plugins/ssr/ssrview.cmi
 ${PLIST.native}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmxs
@@ -926,25 +923,18 @@ lib/coq/plugins/ssrmatching/ssrmatching.glob
 lib/coq/plugins/ssrmatching/ssrmatching.v
 lib/coq/plugins/ssrmatching/ssrmatching.vo
 lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
-lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo
 lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs
 lib/coq/plugins/syntax/ascii_syntax_plugin.cmi
-lib/coq/plugins/syntax/ascii_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
+lib/coq/plugins/syntax/int31_syntax_plugin.cmi
+${PLIST.natdynlink}lib/coq/plugins/syntax/int31_syntax_plugin.cmxs
 lib/coq/plugins/syntax/nat_syntax_plugin.cmi
-lib/coq/plugins/syntax/nat_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
-lib/coq/plugins/syntax/numbers_syntax_plugin.cmi
-lib/coq/plugins/syntax/numbers_syntax_plugin.cmo
-${PLIST.natdynlink}lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs
 lib/coq/plugins/syntax/r_syntax_plugin.cmi
-lib/coq/plugins/syntax/r_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/r_syntax_plugin.cmxs
 lib/coq/plugins/syntax/string_syntax_plugin.cmi
-lib/coq/plugins/syntax/string_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/string_syntax_plugin.cmxs
 lib/coq/plugins/syntax/z_syntax_plugin.cmi
-lib/coq/plugins/syntax/z_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/z_syntax_plugin.cmxs
 lib/coq/pretyping/arguments_renaming.cmi
 lib/coq/pretyping/cases.cmi
@@ -966,7 +956,6 @@ lib/coq/pretyping/nativenorm.cmi
 lib/coq/pretyping/patternops.cmi
 lib/coq/pretyping/pretype_errors.cmi
 ${PLIST.ocaml-opt}lib/coq/pretyping/pretyping.a
-lib/coq/pretyping/pretyping.cma
 lib/coq/pretyping/pretyping.cmi
 ${PLIST.ocaml-opt}lib/coq/pretyping/pretyping.cmxa
 lib/coq/pretyping/program.cmi
@@ -981,34 +970,26 @@ lib/coq/pretyping/typing.cmi
 lib/coq/pretyping/unification.cmi
 lib/coq/pretyping/vnorm.cmi
 lib/coq/printing/genprint.cmi
-lib/coq/printing/miscprint.cmi
-lib/coq/printing/ppannotation.cmi
 lib/coq/printing/ppconstr.cmi
-lib/coq/printing/ppconstrsig.cmi
-lib/coq/printing/pptactic.cmi
-lib/coq/printing/pptacticsig.cmi
 lib/coq/printing/pputils.cmi
 lib/coq/printing/ppvernac.cmi
-lib/coq/printing/ppvernacsig.cmi
 lib/coq/printing/prettyp.cmi
 lib/coq/printing/printer.cmi
 ${PLIST.ocaml-opt}lib/coq/printing/printing.a
-lib/coq/printing/printing.cma
 ${PLIST.ocaml-opt}lib/coq/printing/printing.cmxa
 lib/coq/printing/printmod.cmi
-lib/coq/printing/printmodsig.cmi
 lib/coq/proofs/clenv.cmi
 lib/coq/proofs/clenvtac.cmi
 lib/coq/proofs/evar_refiner.cmi
 lib/coq/proofs/goal.cmi
 lib/coq/proofs/logic.cmi
+lib/coq/proofs/miscprint.cmi
 lib/coq/proofs/pfedit.cmi
 lib/coq/proofs/proof.cmi
 lib/coq/proofs/proof_global.cmi
 lib/coq/proofs/proof_type.cmi
 lib/coq/proofs/proof_using.cmi
 ${PLIST.ocaml-opt}lib/coq/proofs/proofs.a
-lib/coq/proofs/proofs.cma
 ${PLIST.ocaml-opt}lib/coq/proofs/proofs.cmxa
 lib/coq/proofs/redexpr.cmi
 lib/coq/proofs/refine.cmi
@@ -1017,10 +998,8 @@ lib/coq/proofs/tacmach.cmi
 lib/coq/stm/asyncTaskQueue.cmi
 lib/coq/stm/coqworkmgrApi.cmi
 lib/coq/stm/dag.cmi
-lib/coq/stm/lemmas.cmi
 lib/coq/stm/spawned.cmi
 ${PLIST.ocaml-opt}lib/coq/stm/stm.a
-lib/coq/stm/stm.cma
 lib/coq/stm/stm.cmi
 ${PLIST.ocaml-opt}lib/coq/stm/stm.cmxa
 lib/coq/stm/proofBlockDelimiter.cmi
@@ -1028,6 +1007,7 @@ lib/coq/stm/tQueue.cmi
 lib/coq/stm/vcs.cmi
 lib/coq/stm/vernac_classifier.cmi
 lib/coq/stm/vio_checking.cmi
+lib/coq/stm/workerLoop.cmi
 lib/coq/stm/workerPool.cmi
 lib/coq/tactics/auto.cmi
 lib/coq/tactics/autorewrite.cmi
@@ -1044,12 +1024,11 @@ lib/coq/tactics/eqschemes.cmi
 lib/coq/tactics/equality.cmi
 lib/coq/tactics/hints.cmi
 lib/coq/tactics/hipattern.cmi
+lib/coq/tactics/ind_tables.cmi
 lib/coq/tactics/inv.cmi
 lib/coq/tactics/leminv.cmi
-lib/coq/tactics/tactic_matching.cmi
 lib/coq/tactics/tacticals.cmi
 ${PLIST.ocaml-opt}lib/coq/tactics/tactics.a
-lib/coq/tactics/tactics.cma
 lib/coq/tactics/tactics.cmi
 ${PLIST.ocaml-opt}lib/coq/tactics/tactics.cmxa
 lib/coq/tactics/term_dnet.cmi
@@ -1366,10 +1345,6 @@ ${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.o
-${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.o
 ${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmxs
@@ -1382,13 +1357,6 @@ lib/coq/theories/Compat/AdmitAxiom.v
 lib/coq/theories/Compat/AdmitAxiom.glob
 lib/coq/theories/Compat/AdmitAxiom.v
 lib/coq/theories/Compat/AdmitAxiom.vo
-lib/coq/theories/Compat/Coq84.glob
-lib/coq/theories/Compat/Coq84.v
-lib/coq/theories/Compat/Coq84.glob
-lib/coq/theories/Compat/Coq84.v
-lib/coq/theories/Compat/Coq84.vo
-lib/coq/theories/Compat/Coq85.glob
-lib/coq/theories/Compat/Coq85.v
 lib/coq/theories/Compat/Coq85.glob
 lib/coq/theories/Compat/Coq85.v
 lib/coq/theories/Compat/Coq85.vo
@@ -1747,6 +1715,10 @@ ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.o
+${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.o
 ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmxs
@@ -1779,6 +1751,18 @@ ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFac
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFacts.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFacts.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFacts.o
+${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.o
+${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.o
+${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.o
 ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmxs
@@ -1787,6 +1771,10 @@ ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.o
+${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.o
 ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmxs
@@ -1849,6 +1837,9 @@ lib/coq/theories/Logic/EqdepFacts.vo
 lib/coq/theories/Logic/Eqdep_dec.glob
 lib/coq/theories/Logic/Eqdep_dec.v
 lib/coq/theories/Logic/Eqdep_dec.vo
+lib/coq/theories/Logic/ExtensionalFunctionRepresentative.glob
+lib/coq/theories/Logic/ExtensionalFunctionRepresentative.v
+lib/coq/theories/Logic/ExtensionalFunctionRepresentative.vo
 lib/coq/theories/Logic/ExtensionalityFacts.glob
 lib/coq/theories/Logic/ExtensionalityFacts.v
 lib/coq/theories/Logic/ExtensionalityFacts.vo
@@ -1873,12 +1864,24 @@ lib/coq/theories/Logic/ProofIrrelevance.vo
 lib/coq/theories/Logic/ProofIrrelevanceFacts.glob
 lib/coq/theories/Logic/ProofIrrelevanceFacts.v
 lib/coq/theories/Logic/ProofIrrelevanceFacts.vo
+lib/coq/theories/Logic/PropExtensionality.glob
+lib/coq/theories/Logic/PropExtensionality.v
+lib/coq/theories/Logic/PropExtensionality.vo
+lib/coq/theories/Logic/PropExtensionalityFacts.glob
+lib/coq/theories/Logic/PropExtensionalityFacts.v
+lib/coq/theories/Logic/PropExtensionalityFacts.vo
+lib/coq/theories/Logic/PropFacts.glob
+lib/coq/theories/Logic/PropFacts.v
+lib/coq/theories/Logic/PropFacts.vo
 lib/coq/theories/Logic/RelationalChoice.glob
 lib/coq/theories/Logic/RelationalChoice.v
 lib/coq/theories/Logic/RelationalChoice.vo
 lib/coq/theories/Logic/SetIsType.glob
 lib/coq/theories/Logic/SetIsType.v
 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/WKL.glob
 lib/coq/theories/Logic/WKL.v
 lib/coq/theories/Logic/WKL.vo
@@ -2046,10 +2049,6 @@ lib/coq/theories/NArith/Nnat.vo
 lib/coq/theories/NArith/Nsqrt_def.glob
 lib/coq/theories/NArith/Nsqrt_def.v
 lib/coq/theories/NArith/Nsqrt_def.vo
-${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.o
 ${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmxs
@@ -2062,9 +2061,6 @@ ${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.o
-lib/coq/theories/Numbers/BigNumPrelude.glob
-lib/coq/theories/Numbers/BigNumPrelude.v
-lib/coq/theories/Numbers/BigNumPrelude.vo
 lib/coq/theories/Numbers/BinNums.glob
 lib/coq/theories/Numbers/BinNums.v
 lib/coq/theories/Numbers/BinNums.vo
@@ -2072,6 +2068,10 @@ ${PLIST.native}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmxs
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.o
+${PLIST.native}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.o
 ${PLIST.native}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cmxs
@@ -2079,79 +2079,12 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-n
 lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.glob
 lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
 lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
+lib/coq/theories/Numbers/Cyclic/Abstract/DoubleType.glob
+lib/coq/theories/Numbers/Cyclic/Abstract/DoubleType.v
+lib/coq/theories/Numbers/Cyclic/Abstract/DoubleType.vo
 lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.glob
 lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.v
 lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.o
-${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.o
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.glob
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
-lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
 ${PLIST.native}lib/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmxs
@@ -2306,20 +2239,6 @@ lib/coq/theories/Numbers/Integer/Abstract/ZProperties.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.glob
 lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.v
 lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
-${PLIST.native}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.o
-${PLIST.native}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.o
-lib/coq/theories/Numbers/Integer/BigZ/BigZ.glob
-lib/coq/theories/Numbers/Integer/BigZ/BigZ.v
-lib/coq/theories/Numbers/Integer/BigZ/BigZ.vo
-lib/coq/theories/Numbers/Integer/BigZ/ZMake.glob
-lib/coq/theories/Numbers/Integer/BigZ/ZMake.v
-lib/coq/theories/Numbers/Integer/BigZ/ZMake.vo
 ${PLIST.native}lib/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmxs
@@ -2334,20 +2253,6 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/NatPairs/.coq-
 lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.glob
 lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.v
 lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vo
-${PLIST.native}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.o
-${PLIST.native}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.o
-lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.glob
-lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.v
-lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.vo
-lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.glob
-lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
-lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo
 lib/coq/theories/Numbers/NaryFunctions.glob
 lib/coq/theories/Numbers/NaryFunctions.v
 lib/coq/theories/Numbers/NaryFunctions.vo
@@ -2603,34 +2508,6 @@ lib/coq/theories/Numbers/Natural/Abstract/NStrongRec.vo
 lib/coq/theories/Numbers/Natural/Abstract/NSub.glob
 lib/coq/theories/Numbers/Natural/Abstract/NSub.v
 lib/coq/theories/Numbers/Natural/Abstract/NSub.vo
-${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.o
-${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.o
-${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.o
-${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.o
-lib/coq/theories/Numbers/Natural/BigN/BigN.glob
-lib/coq/theories/Numbers/Natural/BigN/BigN.v
-lib/coq/theories/Numbers/Natural/BigN/BigN.vo
-lib/coq/theories/Numbers/Natural/BigN/NMake.glob
-lib/coq/theories/Numbers/Natural/BigN/NMake.v
-lib/coq/theories/Numbers/Natural/BigN/NMake.vo
-lib/coq/theories/Numbers/Natural/BigN/NMake_gen.glob
-lib/coq/theories/Numbers/Natural/BigN/NMake_gen.v
-lib/coq/theories/Numbers/Natural/BigN/NMake_gen.vo
-lib/coq/theories/Numbers/Natural/BigN/Nbasic.glob
-lib/coq/theories/Numbers/Natural/BigN/Nbasic.v
-lib/coq/theories/Numbers/Natural/BigN/Nbasic.vo
 ${PLIST.native}lib/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmxs
@@ -2645,44 +2522,9 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/Peano/.coq-nat
 lib/coq/theories/Numbers/Natural/Peano/NPeano.glob
 lib/coq/theories/Numbers/Natural/Peano/NPeano.v
 lib/coq/theories/Numbers/Natural/Peano/NPeano.vo
-${PLIST.native}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.o
-${PLIST.native}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.o
-lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.glob
-lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.v
-lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.vo
-lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.glob
-lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
-lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo
 lib/coq/theories/Numbers/NumPrelude.glob
 lib/coq/theories/Numbers/NumPrelude.v
 lib/coq/theories/Numbers/NumPrelude.vo
-${PLIST.native}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.o
-${PLIST.native}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.o
-lib/coq/theories/Numbers/Rational/BigQ/BigQ.glob
-lib/coq/theories/Numbers/Rational/BigQ/BigQ.v
-lib/coq/theories/Numbers/Rational/BigQ/BigQ.vo
-lib/coq/theories/Numbers/Rational/BigQ/QMake.glob
-lib/coq/theories/Numbers/Rational/BigQ/QMake.v
-lib/coq/theories/Numbers/Rational/BigQ/QMake.vo
-${PLIST.native}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.o
-lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.glob
-lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.v
-lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.vo
 ${PLIST.native}lib/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmxs
@@ -3999,41 +3841,46 @@ lib/coq/theories/ZArith/Zwf.vo
 lib/coq/theories/ZArith/auxiliary.glob
 lib/coq/theories/ZArith/auxiliary.v
 lib/coq/theories/ZArith/auxiliary.vo
+lib/coq/tools/CoqMakefile.in
+lib/coq/tools/TimeFileMaker.py
 lib/coq/tools/coqdoc/coqdoc.css
 lib/coq/tools/coqdoc/coqdoc.sty
-lib/coq/toplevel/assumptions.cmi
-lib/coq/toplevel/auto_ind_decl.cmi
-lib/coq/toplevel/class.cmi
-lib/coq/toplevel/classes.cmi
-lib/coq/toplevel/command.cmi
+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
 lib/coq/toplevel/coqinit.cmi
 lib/coq/toplevel/coqloop.cmi
 lib/coq/toplevel/coqtop.cmi
-lib/coq/toplevel/discharge.cmi
-lib/coq/toplevel/explainErr.cmi
-lib/coq/toplevel/himsg.cmi
-lib/coq/toplevel/ind_tables.cmi
-lib/coq/toplevel/indschemes.cmi
-lib/coq/toplevel/locality.cmi
-lib/coq/toplevel/metasyntax.cmi
-lib/coq/toplevel/mltop.cmi
-lib/coq/toplevel/obligations.cmi
-lib/coq/toplevel/record.cmi
-lib/coq/toplevel/search.cmi
 ${PLIST.ocaml-opt}lib/coq/toplevel/toplevel.a
-lib/coq/toplevel/toplevel.cma
 ${PLIST.ocaml-opt}lib/coq/toplevel/toplevel.cmxa
 lib/coq/toplevel/usage.cmi
 lib/coq/toplevel/vernac.cmi
-lib/coq/toplevel/vernacentries.cmi
-lib/coq/toplevel/vernacinterp.cmi
-${PLIST.ocaml-opt}${PLIST.coqide}lib/coq/toploop/coqidetop.cma
+lib/coq/vernac/assumptions.cmi
+lib/coq/vernac/auto_ind_decl.cmi
+lib/coq/vernac/class.cmi
+lib/coq/vernac/classes.cmi
+lib/coq/vernac/command.cmi
+lib/coq/vernac/declareDef.cmi
+lib/coq/vernac/discharge.cmi
+lib/coq/vernac/explainErr.cmi
+lib/coq/vernac/himsg.cmi
+lib/coq/vernac/indschemes.cmi
+lib/coq/vernac/lemmas.cmi
+lib/coq/vernac/locality.cmi
+lib/coq/vernac/metasyntax.cmi
+lib/coq/vernac/mltop.cmi
+lib/coq/vernac/obligations.cmi
+lib/coq/vernac/record.cmi
+lib/coq/vernac/search.cmi
+lib/coq/vernac/topfmt.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/vernac.a
+${PLIST.ocaml-opt}lib/coq/vernac/vernac.cmxa
+lib/coq/vernac/vernacentries.cmi
+lib/coq/vernac/vernacinterp.cmi
+lib/coq/vernac/vernacprop.cmi
 ${PLIST.natdynlink}${PLIST.coqide}lib/coq/toploop/coqidetop.cmxs
-${PLIST.ocaml-opt}lib/coq/toploop/proofworkertop.cma
 ${PLIST.natdynlink}lib/coq/toploop/proofworkertop.cmxs
-${PLIST.ocaml-opt}lib/coq/toploop/queryworkertop.cma
 ${PLIST.natdynlink}lib/coq/toploop/queryworkertop.cmxs
-${PLIST.ocaml-opt}lib/coq/toploop/tacworkertop.cma
 ${PLIST.natdynlink}lib/coq/toploop/tacworkertop.cmxs
 man/man1/coq-tex.1
 man/man1/coq_makefile.1
@@ -4048,11 +3895,11 @@ man/man1/coqtop.byte.1
 man/man1/coqtop.opt.1
 man/man1/coqwc.1
 man/man1/gallina.1
-share/coq/coq-ssreflect.lang
-share/coq/coq.lang
-share/coq/coq.png
-share/coq/coq_style.xml
-share/doc/coq/FAQ-CoqIde
+${PLIST.coqide}share/coq/coq-ssreflect.lang
+${PLIST.coqide}share/coq/coq.lang
+${PLIST.coqide}share/coq/coq.png
+${PLIST.coqide}share/coq/coq_style.xml
+${PLIST.coqide}share/doc/coq/FAQ-CoqIde
 ${PLIST.doc}share/doc/coq/LICENSE.doc
 ${PLIST.doc}share/doc/coq/html/RecTutorial.html
 ${PLIST.doc}share/doc/coq/html/Tutorial.html
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 5f09c916acc..7b96b4ebf83 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,8 +1,9 @@
-$NetBSD: distinfo,v 1.27 2017/09/08 17:19:01 jaapb Exp $
+$NetBSD: distinfo,v 1.28 2017/11/03 11:20:28 jaapb Exp $
 
-SHA1 (coq-8.6.1.tar.gz) = 5dbaf1230c297d7c11c8715c012300a51ad80f9a
-RMD160 (coq-8.6.1.tar.gz) = 822b0061a99de144881b1f1166eef9e92d26de7f
-SHA512 (coq-8.6.1.tar.gz) = 814ab76a06ca15f927081428da74add4bc67290199fa011853b9c68a00cdefaf813b10fbac18a434f4504fce8f2173eb544080bf6f50d62caa41bb8724b13083
-Size (coq-8.6.1.tar.gz) = 5588811 bytes
-SHA1 (patch-Makefile.common) = 79b02edff66ddcfb267816b0031c724620e67a13
+SHA1 (coq-8.7.0.tar.gz) = b539e0ff6f2a6dd31bbe8856db152705f9a22a01
+RMD160 (coq-8.7.0.tar.gz) = 7e752473b27a2d1a0f95ea3eb258ffba5a5a8d4f
+SHA512 (coq-8.7.0.tar.gz) = c806881d1ab823d9c2d748aa2d7fd3faaa0f6395536942ad214c68658b2688e6c57941947a440ddb69bf1436249067eefd866ecb1d9e4c5e774e3218c80a6fc2
+Size (coq-8.7.0.tar.gz) = 5629204 bytes
+SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc
 SHA1 (patch-configure.ml) = 8e48a65709234281e3898ebae9041dfc04c7fe7b
+SHA1 (patch-ide_ideutils.ml) = 7fd59bcfc0cf4f65fd7f4e5a0ec95cb694df8417
diff --git a/lang/coq/patches/patch-Makefile.common b/lang/coq/patches/patch-Makefile.common
index 11f2babbc12..34eca2d6302 100644
--- a/lang/coq/patches/patch-Makefile.common
+++ b/lang/coq/patches/patch-Makefile.common
@@ -1,13 +1,15 @@
-$NetBSD: patch-Makefile.common,v 1.3 2016/12/30 13:23:06 jaapb Exp $
+$NetBSD: patch-Makefile.common,v 1.4 2017/11/03 11:20:28 jaapb Exp $
 
 Use BSD_INSTALL_*
---- Makefile.common.orig	2016-10-25 20:17:16.000000000 +0000
+--- Makefile.common.orig	2017-10-16 08:53:18.000000000 +0000
 +++ Makefile.common
-@@ -35,7 +35,7 @@ else
+@@ -69,8 +69,8 @@ DYNOBJ:=.cmo
+ DYNLIB:=.cma
  endif
  
- INSTALLBIN:=install
--INSTALLLIB:=install -m 644 
+-INSTALLBIN:=install
+-INSTALLLIB:=install -m 644
++INSTALLBIN:=${BSD_INSTALL_PROGRAM}
 +INSTALLLIB:=${BSD_INSTALL_LIB}
  INSTALLSH:=./install.sh
  MKDIR:=install -d
diff --git a/lang/coq/patches/patch-ide_ideutils.ml b/lang/coq/patches/patch-ide_ideutils.ml
new file mode 100644
index 00000000000..5720dfc4c0a
--- /dev/null
+++ b/lang/coq/patches/patch-ide_ideutils.ml
@@ -0,0 +1,14 @@
+$NetBSD: patch-ide_ideutils.ml,v 1.1 2017/11/03 11:20:28 jaapb Exp $
+
+For compilation with lablgtk 2.18.6
+--- ide/ideutils.ml.orig	2017-10-16 08:53:18.000000000 +0000
++++ ide/ideutils.ml
+@@ -373,7 +373,7 @@ let io_read_all chan =
+   Buffer.clear read_buffer;
+   let read_once () =
+     (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *)
+-    let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in
++    let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in
+     Buffer.add_subbytes read_buffer read_string 0 len
+   in
+   begin