Updated package lang/coq to version 8.7.1.

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

6 files changed, 587 insertions, 109 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index 0ddab7cb9de..788ef1f4c23 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.103 2017/11/30 16:45:28 adam Exp $
+# $NetBSD: Makefile,v 1.104 2018/01/10 16:26:53 jaapb Exp $
 #
 
-DISTNAME=	coq-8.7.0
-PKGREVISION=	2
+DISTNAME=	coq-8.7.1
 CATEGORIES=	lang math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -75,7 +74,7 @@ SUBST_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 b351d895549..d0417d87c43 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.23 2018/01/01 22:29:39 rillig Exp $
+@comment $NetBSD: PLIST,v 1.24 2018/01/10 16:26:53 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -13,20 +13,33 @@ bin/coqworkmgr
 bin/gallina
 lib/coq/META
 lib/coq/config/coq_config.cmi
+${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx
 lib/coq/engine/eConstr.cmi
+${PLIST.ocaml-opt}lib/coq/engine/eConstr.cmx
 ${PLIST.ocaml-opt}lib/coq/engine/engine.a
 ${PLIST.ocaml-opt}lib/coq/engine/engine.cmxa
 lib/coq/engine/evarutil.cmi
+${PLIST.ocaml-opt}lib/coq/engine/evarutil.cmx
 lib/coq/engine/evd.cmi
+${PLIST.ocaml-opt}lib/coq/engine/evd.cmx
 lib/coq/engine/ftactic.cmi
+${PLIST.ocaml-opt}lib/coq/engine/ftactic.cmx
 lib/coq/engine/geninterp.cmi
+${PLIST.ocaml-opt}lib/coq/engine/geninterp.cmx
 lib/coq/engine/logic_monad.cmi
+${PLIST.ocaml-opt}lib/coq/engine/logic_monad.cmx
 lib/coq/engine/namegen.cmi
+${PLIST.ocaml-opt}lib/coq/engine/namegen.cmx
 lib/coq/engine/proofview.cmi
+${PLIST.ocaml-opt}lib/coq/engine/proofview.cmx
 lib/coq/engine/proofview_monad.cmi
+${PLIST.ocaml-opt}lib/coq/engine/proofview_monad.cmx
 lib/coq/engine/termops.cmi
+${PLIST.ocaml-opt}lib/coq/engine/termops.cmx
 lib/coq/engine/uState.cmi
+${PLIST.ocaml-opt}lib/coq/engine/uState.cmx
 lib/coq/engine/universes.cmi
+${PLIST.ocaml-opt}lib/coq/engine/universes.cmx
 lib/coq/grammar/grammar.cma
 lib/coq/grammar/q_util.cmi
 ${PLIST.coqide}lib/coq/ide/config_lexer.cmi
@@ -68,185 +81,343 @@ ${PLIST.coqide}lib/coq/ide/xml_parser.cmi
 ${PLIST.coqide}lib/coq/ide/xml_printer.cmi
 ${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
 lib/coq/interp/constrexpr_ops.cmi
+${PLIST.ocaml-opt}lib/coq/interp/constrexpr_ops.cmx
 lib/coq/interp/constrextern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/constrextern.cmx
 lib/coq/interp/constrintern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/constrintern.cmx
 lib/coq/interp/declare.cmi
+${PLIST.ocaml-opt}lib/coq/interp/declare.cmx
 lib/coq/interp/dumpglob.cmi
+${PLIST.ocaml-opt}lib/coq/interp/dumpglob.cmx
 lib/coq/interp/genintern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/genintern.cmx
 lib/coq/interp/impargs.cmi
+${PLIST.ocaml-opt}lib/coq/interp/impargs.cmx
 lib/coq/interp/implicit_quantifiers.cmi
+${PLIST.ocaml-opt}lib/coq/interp/implicit_quantifiers.cmx
 ${PLIST.ocaml-opt}lib/coq/interp/interp.a
 ${PLIST.ocaml-opt}lib/coq/interp/interp.cmxa
 lib/coq/interp/modintern.cmi
+${PLIST.ocaml-opt}lib/coq/interp/modintern.cmx
 lib/coq/interp/notation.cmi
+${PLIST.ocaml-opt}lib/coq/interp/notation.cmx
 lib/coq/interp/notation_ops.cmi
+${PLIST.ocaml-opt}lib/coq/interp/notation_ops.cmx
 lib/coq/interp/ppextend.cmi
+${PLIST.ocaml-opt}lib/coq/interp/ppextend.cmx
 lib/coq/interp/reserve.cmi
+${PLIST.ocaml-opt}lib/coq/interp/reserve.cmx
 lib/coq/interp/smartlocate.cmi
+${PLIST.ocaml-opt}lib/coq/interp/smartlocate.cmx
 lib/coq/interp/stdarg.cmi
+${PLIST.ocaml-opt}lib/coq/interp/stdarg.cmx
 lib/coq/interp/syntax_def.cmi
+${PLIST.ocaml-opt}lib/coq/interp/syntax_def.cmx
 lib/coq/interp/topconstr.cmi
+${PLIST.ocaml-opt}lib/coq/interp/topconstr.cmx
 lib/coq/intf/constrexpr.cmi
+${PLIST.ocaml-opt}lib/coq/intf/constrexpr.cmx
 lib/coq/intf/decl_kinds.cmi
+${PLIST.ocaml-opt}lib/coq/intf/decl_kinds.cmx
 lib/coq/intf/evar_kinds.cmi
+${PLIST.ocaml-opt}lib/coq/intf/evar_kinds.cmx
 lib/coq/intf/extend.cmi
+${PLIST.ocaml-opt}lib/coq/intf/extend.cmx
 lib/coq/intf/genredexpr.cmi
+${PLIST.ocaml-opt}lib/coq/intf/genredexpr.cmx
 lib/coq/intf/glob_term.cmi
+${PLIST.ocaml-opt}lib/coq/intf/glob_term.cmx
 ${PLIST.ocaml-opt}lib/coq/intf/intf.a
 ${PLIST.ocaml-opt}lib/coq/intf/intf.cmxa
 lib/coq/intf/locus.cmi
+${PLIST.ocaml-opt}lib/coq/intf/locus.cmx
 lib/coq/intf/misctypes.cmi
+${PLIST.ocaml-opt}lib/coq/intf/misctypes.cmx
 lib/coq/intf/notation_term.cmi
+${PLIST.ocaml-opt}lib/coq/intf/notation_term.cmx
 lib/coq/intf/pattern.cmi
+${PLIST.ocaml-opt}lib/coq/intf/pattern.cmx
 lib/coq/intf/tactypes.cmi
+${PLIST.ocaml-opt}lib/coq/intf/tactypes.cmx
 lib/coq/intf/vernacexpr.cmi
+${PLIST.ocaml-opt}lib/coq/intf/vernacexpr.cmx
 lib/coq/kernel/byterun/dllcoqrun.so
-lib/coq/kernel/byterun/libcoqrun.a
+${PLIST.ocaml-opt}lib/coq/kernel/byterun/libcoqrun.a
 lib/coq/kernel/cClosure.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cClosure.cmx
 lib/coq/kernel/cbytecodes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cbytecodes.cmx
 lib/coq/kernel/cbytegen.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cbytegen.cmx
 lib/coq/kernel/cemitcodes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cemitcodes.cmx
 lib/coq/kernel/constr.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/constr.cmx
 lib/coq/kernel/context.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/context.cmx
 lib/coq/kernel/conv_oracle.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/conv_oracle.cmx
 lib/coq/kernel/cooking.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/cooking.cmx
 lib/coq/kernel/copcodes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/copcodes.cmx
 lib/coq/kernel/csymtable.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/csymtable.cmx
 lib/coq/kernel/declarations.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/declarations.cmx
 lib/coq/kernel/declareops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/declareops.cmx
 lib/coq/kernel/entries.cmi
 lib/coq/kernel/environ.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/environ.cmx
 lib/coq/kernel/esubst.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/esubst.cmx
 lib/coq/kernel/evar.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/evar.cmx
 lib/coq/kernel/indtypes.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/indtypes.cmx
 lib/coq/kernel/inductive.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/inductive.cmx
 ${PLIST.ocaml-opt}lib/coq/kernel/kernel.a
 ${PLIST.ocaml-opt}lib/coq/kernel/kernel.cmxa
 lib/coq/kernel/mod_subst.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/mod_subst.cmx
 lib/coq/kernel/mod_typing.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/mod_typing.cmx
 lib/coq/kernel/modops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/modops.cmx
 lib/coq/kernel/names.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/names.cmx
 lib/coq/kernel/nativecode.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativecode.cmx
 lib/coq/kernel/nativeconv.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativeconv.cmx
 lib/coq/kernel/nativeinstr.cmi
 lib/coq/kernel/nativelambda.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativelambda.cmx
 lib/coq/kernel/nativelib.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativelib.cmx
 lib/coq/kernel/nativelibrary.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativelibrary.cmx
 lib/coq/kernel/nativevalues.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/nativevalues.cmx
 lib/coq/kernel/opaqueproof.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/opaqueproof.cmx
 lib/coq/kernel/pre_env.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/pre_env.cmx
 lib/coq/kernel/primitives.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/primitives.cmx
 lib/coq/kernel/reduction.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/reduction.cmx
 lib/coq/kernel/retroknowledge.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/retroknowledge.cmx
 lib/coq/kernel/safe_typing.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/safe_typing.cmx
 lib/coq/kernel/sorts.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/sorts.cmx
 lib/coq/kernel/subtyping.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/subtyping.cmx
 lib/coq/kernel/term.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/term.cmx
 lib/coq/kernel/term_typing.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/term_typing.cmx
 lib/coq/kernel/type_errors.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/type_errors.cmx
 lib/coq/kernel/typeops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/typeops.cmx
 lib/coq/kernel/uGraph.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/uGraph.cmx
 lib/coq/kernel/uint31.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/uint31.cmx
 lib/coq/kernel/univ.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/univ.cmx
 lib/coq/kernel/vars.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/vars.cmx
 lib/coq/kernel/vconv.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/vconv.cmx
 lib/coq/kernel/vm.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/vm.cmx
 lib/coq/lib/aux_file.cmi
+${PLIST.ocaml-opt}lib/coq/lib/aux_file.cmx
 lib/coq/lib/backtrace.cmi
+${PLIST.ocaml-opt}lib/coq/lib/backtrace.cmx
 lib/coq/lib/bigint.cmi
+${PLIST.ocaml-opt}lib/coq/lib/bigint.cmx
 lib/coq/lib/cArray.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cArray.cmx
 lib/coq/lib/cAst.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cAst.cmx
 lib/coq/lib/cEphemeron.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cEphemeron.cmx
 lib/coq/lib/cErrors.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cErrors.cmx
 lib/coq/lib/cList.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cList.cmx
 lib/coq/lib/cMap.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cMap.cmx
 lib/coq/lib/cObj.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cObj.cmx
 lib/coq/lib/cSet.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cSet.cmx
 lib/coq/lib/cSig.cmi
 lib/coq/lib/cStack.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cStack.cmx
 lib/coq/lib/cString.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cString.cmx
 lib/coq/lib/cThread.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cThread.cmx
 lib/coq/lib/cUnix.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cUnix.cmx
 lib/coq/lib/cWarnings.cmi
+${PLIST.ocaml-opt}lib/coq/lib/cWarnings.cmx
 lib/coq/lib/canary.cmi
+${PLIST.ocaml-opt}lib/coq/lib/canary.cmx
 ${PLIST.ocaml-opt}lib/coq/lib/clib.a
 ${PLIST.ocaml-opt}lib/coq/lib/clib.cmxa
 lib/coq/lib/control.cmi
+${PLIST.ocaml-opt}lib/coq/lib/control.cmx
 lib/coq/lib/coqProject_file.cmi
+${PLIST.ocaml-opt}lib/coq/lib/coqProject_file.cmx
 lib/coq/lib/deque.cmi
+${PLIST.ocaml-opt}lib/coq/lib/deque.cmx
 lib/coq/lib/dyn.cmi
+${PLIST.ocaml-opt}lib/coq/lib/dyn.cmx
 lib/coq/lib/envars.cmi
+${PLIST.ocaml-opt}lib/coq/lib/envars.cmx
 lib/coq/lib/exninfo.cmi
+${PLIST.ocaml-opt}lib/coq/lib/exninfo.cmx
 lib/coq/lib/explore.cmi
+${PLIST.ocaml-opt}lib/coq/lib/explore.cmx
 lib/coq/lib/feedback.cmi
+${PLIST.ocaml-opt}lib/coq/lib/feedback.cmx
 lib/coq/lib/flags.cmi
+${PLIST.ocaml-opt}lib/coq/lib/flags.cmx
 lib/coq/lib/future.cmi
+${PLIST.ocaml-opt}lib/coq/lib/future.cmx
 lib/coq/lib/genarg.cmi
+${PLIST.ocaml-opt}lib/coq/lib/genarg.cmx
 lib/coq/lib/hMap.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hMap.cmx
 lib/coq/lib/hashcons.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hashcons.cmx
 lib/coq/lib/hashset.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hashset.cmx
 lib/coq/lib/heap.cmi
+${PLIST.ocaml-opt}lib/coq/lib/heap.cmx
 lib/coq/lib/hook.cmi
+${PLIST.ocaml-opt}lib/coq/lib/hook.cmx
 lib/coq/lib/iStream.cmi
+${PLIST.ocaml-opt}lib/coq/lib/iStream.cmx
 lib/coq/lib/int.cmi
+${PLIST.ocaml-opt}lib/coq/lib/int.cmx
 ${PLIST.ocaml-opt}lib/coq/lib/lib.a
 ${PLIST.ocaml-opt}lib/coq/lib/lib.cmxa
 lib/coq/lib/loc.cmi
+${PLIST.ocaml-opt}lib/coq/lib/loc.cmx
 lib/coq/lib/minisys.cmi
+${PLIST.ocaml-opt}lib/coq/lib/minisys.cmx
 lib/coq/lib/monad.cmi
+${PLIST.ocaml-opt}lib/coq/lib/monad.cmx
 lib/coq/lib/option.cmi
+${PLIST.ocaml-opt}lib/coq/lib/option.cmx
 lib/coq/lib/pp.cmi
+${PLIST.ocaml-opt}lib/coq/lib/pp.cmx
 lib/coq/lib/predicate.cmi
+${PLIST.ocaml-opt}lib/coq/lib/predicate.cmx
 lib/coq/lib/profile.cmi
+${PLIST.ocaml-opt}lib/coq/lib/profile.cmx
 lib/coq/lib/remoteCounter.cmi
+${PLIST.ocaml-opt}lib/coq/lib/remoteCounter.cmx
 lib/coq/lib/rtree.cmi
+${PLIST.ocaml-opt}lib/coq/lib/rtree.cmx
 lib/coq/lib/segmenttree.cmi
+${PLIST.ocaml-opt}lib/coq/lib/segmenttree.cmx
 lib/coq/lib/spawn.cmi
+${PLIST.ocaml-opt}lib/coq/lib/spawn.cmx
 lib/coq/lib/stateid.cmi
+${PLIST.ocaml-opt}lib/coq/lib/stateid.cmx
 lib/coq/lib/store.cmi
+${PLIST.ocaml-opt}lib/coq/lib/store.cmx
 lib/coq/lib/system.cmi
+${PLIST.ocaml-opt}lib/coq/lib/system.cmx
 lib/coq/lib/terminal.cmi
+${PLIST.ocaml-opt}lib/coq/lib/terminal.cmx
 lib/coq/lib/trie.cmi
+${PLIST.ocaml-opt}lib/coq/lib/trie.cmx
 lib/coq/lib/unicode.cmi
+${PLIST.ocaml-opt}lib/coq/lib/unicode.cmx
 lib/coq/lib/unicodetable.cmi
+${PLIST.ocaml-opt}lib/coq/lib/unicodetable.cmx
 lib/coq/lib/unionfind.cmi
+${PLIST.ocaml-opt}lib/coq/lib/unionfind.cmx
 lib/coq/lib/util.cmi
+${PLIST.ocaml-opt}lib/coq/lib/util.cmx
 lib/coq/lib/xml_datatype.cmi
 lib/coq/library/coqlib.cmi
+${PLIST.ocaml-opt}lib/coq/library/coqlib.cmx
 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
+${PLIST.ocaml-opt}lib/coq/library/globnames.cmx
 lib/coq/library/goptions.cmi
+${PLIST.ocaml-opt}lib/coq/library/goptions.cmx
 lib/coq/library/heads.cmi
+${PLIST.ocaml-opt}lib/coq/library/heads.cmx
 lib/coq/library/keys.cmi
+${PLIST.ocaml-opt}lib/coq/library/keys.cmx
 lib/coq/library/kindops.cmi
+${PLIST.ocaml-opt}lib/coq/library/kindops.cmx
 lib/coq/library/lib.cmi
+${PLIST.ocaml-opt}lib/coq/library/lib.cmx
 lib/coq/library/libnames.cmi
+${PLIST.ocaml-opt}lib/coq/library/libnames.cmx
 lib/coq/library/libobject.cmi
+${PLIST.ocaml-opt}lib/coq/library/libobject.cmx
 ${PLIST.ocaml-opt}lib/coq/library/library.a
 lib/coq/library/library.cmi
+${PLIST.ocaml-opt}lib/coq/library/library.cmx
 ${PLIST.ocaml-opt}lib/coq/library/library.cmxa
 lib/coq/library/loadpath.cmi
+${PLIST.ocaml-opt}lib/coq/library/loadpath.cmx
 lib/coq/library/nameops.cmi
+${PLIST.ocaml-opt}lib/coq/library/nameops.cmx
 lib/coq/library/nametab.cmi
+${PLIST.ocaml-opt}lib/coq/library/nametab.cmx
 lib/coq/library/states.cmi
+${PLIST.ocaml-opt}lib/coq/library/states.cmx
 lib/coq/library/summary.cmi
+${PLIST.ocaml-opt}lib/coq/library/summary.cmx
 lib/coq/library/univops.cmi
+${PLIST.ocaml-opt}lib/coq/library/univops.cmx
 lib/coq/parsing/cLexer.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/cLexer.cmx
 lib/coq/parsing/egramcoq.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/egramcoq.cmx
 lib/coq/parsing/egramml.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/egramml.cmx
 lib/coq/parsing/g_constr.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/g_constr.cmx
 lib/coq/parsing/g_prim.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/g_prim.cmx
 lib/coq/parsing/g_proofs.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/g_proofs.cmx
 lib/coq/parsing/g_vernac.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/g_vernac.cmx
 ${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
+${PLIST.ocaml-opt}lib/coq/parsing/pcoq.cmx
 lib/coq/parsing/tok.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/tok.cmx
 ${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
@@ -270,21 +441,32 @@ lib/coq/plugins/btauto/Reflect.v
 lib/coq/plugins/btauto/Reflect.vo
 lib/coq/plugins/btauto/btauto_plugin.cmi
 ${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
+${PLIST.ocaml-opt}lib/coq/plugins/btauto/refl_btauto.cmx
 lib/coq/plugins/cc/cc_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/cc/cc_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/cc/cc_plugin.o
 lib/coq/plugins/cc/ccalgo.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/cc/ccalgo.cmx
 lib/coq/plugins/cc/ccproof.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/cc/ccproof.cmx
 lib/coq/plugins/cc/cctac.cmi
-lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmx
-${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
+${PLIST.ocaml-opt}lib/coq/plugins/cc/cctac.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/cc/g_congruence.cmx
+${PLIST.native}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmxs
+${PLIST.native}${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
+${PLIST.ocaml-opt}lib/coq/plugins/derive/derive.cmx
 lib/coq/plugins/derive/derive_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/derive/derive_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/derive/derive_plugin.o
+${PLIST.ocaml-opt}lib/coq/plugins/derive/g_derive.cmx
 ${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
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmxs
@@ -405,26 +587,46 @@ lib/coq/plugins/extraction/Extraction.glob
 lib/coq/plugins/extraction/Extraction.v
 lib/coq/plugins/extraction/Extraction.vo
 lib/coq/plugins/extraction/common.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/common.cmx
 lib/coq/plugins/extraction/extract_env.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/extract_env.cmx
 lib/coq/plugins/extraction/extraction.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/extraction.cmx
 lib/coq/plugins/extraction/extraction_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/extraction/extraction_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/extraction_plugin.o
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/g_extraction.cmx
 lib/coq/plugins/extraction/haskell.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/haskell.cmx
 lib/coq/plugins/extraction/json.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/json.cmx
 lib/coq/plugins/extraction/miniml.cmi
 lib/coq/plugins/extraction/mlutil.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/mlutil.cmx
 lib/coq/plugins/extraction/modutil.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/modutil.cmx
 lib/coq/plugins/extraction/ocaml.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/ocaml.cmx
 lib/coq/plugins/extraction/scheme.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/scheme.cmx
 lib/coq/plugins/extraction/table.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/table.cmx
 lib/coq/plugins/firstorder/formula.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/formula.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/g_ground.cmx
 lib/coq/plugins/firstorder/ground.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/ground.cmx
 lib/coq/plugins/firstorder/ground_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/firstorder/ground_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/ground_plugin.o
 lib/coq/plugins/firstorder/instances.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/instances.cmx
 lib/coq/plugins/firstorder/rules.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/rules.cmx
 lib/coq/plugins/firstorder/sequent.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/sequent.cmx
 lib/coq/plugins/firstorder/unify.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/unify.cmx
 ${PLIST.native}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmxs
@@ -439,8 +641,12 @@ lib/coq/plugins/fourier/Fourier.vo
 lib/coq/plugins/fourier/Fourier_util.glob
 lib/coq/plugins/fourier/Fourier_util.v
 lib/coq/plugins/fourier/Fourier_util.vo
+${PLIST.ocaml-opt}lib/coq/plugins/fourier/fourier.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/fourier/fourierR.cmx
 lib/coq/plugins/fourier/fourier_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/fourier/fourier_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/fourier/fourier_plugin.o
+${PLIST.ocaml-opt}lib/coq/plugins/fourier/g_fourier.cmx
 ${PLIST.native}lib/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmxs
@@ -456,14 +662,25 @@ lib/coq/plugins/funind/Recdef.glob
 lib/coq/plugins/funind/Recdef.v
 lib/coq/plugins/funind/Recdef.vo
 lib/coq/plugins/funind/functional_principles_proofs.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/functional_principles_proofs.cmx
 lib/coq/plugins/funind/functional_principles_types.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/functional_principles_types.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/funind/g_indfun.cmx
 lib/coq/plugins/funind/glob_term_to_relation.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/glob_term_to_relation.cmx
 lib/coq/plugins/funind/glob_termops.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/glob_termops.cmx
 lib/coq/plugins/funind/indfun.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/indfun.cmx
 lib/coq/plugins/funind/indfun_common.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/indfun_common.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/funind/invfun.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/funind/merge.cmx
 lib/coq/plugins/funind/recdef.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/recdef.cmx
 lib/coq/plugins/funind/recdef_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/funind/recdef_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/funind/recdef_plugin.o
 ${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
@@ -471,29 +688,58 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac
 lib/coq/plugins/ltac/Ltac.glob
 lib/coq/plugins/ltac/Ltac.v
 lib/coq/plugins/ltac/Ltac.vo
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/coretactics.cmx
 lib/coq/plugins/ltac/evar_tactics.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/evar_tactics.cmx
 lib/coq/plugins/ltac/extraargs.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/extraargs.cmx
 lib/coq/plugins/ltac/extratactics.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/extratactics.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_auto.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_class.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_eqdecide.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_ltac.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_obligations.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_rewrite.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_tactic.cmx
 lib/coq/plugins/ltac/ltac_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/ltac/ltac_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/ltac_plugin.o
 lib/coq/plugins/ltac/pltac.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/pltac.cmx
 lib/coq/plugins/ltac/pptactic.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/pptactic.cmx
 lib/coq/plugins/ltac/profile_ltac.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/profile_ltac.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/profile_ltac_tactics.cmx
 lib/coq/plugins/ltac/rewrite.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/rewrite.cmx
 lib/coq/plugins/ltac/tacarg.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacarg.cmx
 lib/coq/plugins/ltac/taccoerce.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/taccoerce.cmx
 lib/coq/plugins/ltac/tacentries.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacentries.cmx
 lib/coq/plugins/ltac/tacenv.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacenv.cmx
 lib/coq/plugins/ltac/tacexpr.cmi
 lib/coq/plugins/ltac/tacintern.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacintern.cmx
 lib/coq/plugins/ltac/tacinterp.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacinterp.cmx
 lib/coq/plugins/ltac/tacsubst.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacsubst.cmx
 lib/coq/plugins/ltac/tactic_debug.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tactic_debug.cmx
 lib/coq/plugins/ltac/tactic_matching.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tactic_matching.cmx
 lib/coq/plugins/ltac/tactic_option.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tactic_option.cmx
 lib/coq/plugins/ltac/tauto.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tauto.cmx
 lib/coq/plugins/ltac/tauto_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/ltac/tauto_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tauto_plugin.o
 ${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
@@ -606,12 +852,25 @@ lib/coq/plugins/micromega/ZCoeff.vo
 lib/coq/plugins/micromega/ZMicromega.glob
 lib/coq/plugins/micromega/ZMicromega.v
 lib/coq/plugins/micromega/ZMicromega.vo
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/certificate.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/coq_micromega.cmx
 lib/coq/plugins/micromega/csdpcert
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/csdpcert.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/g_micromega.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/mfourier.cmx
 lib/coq/plugins/micromega/micromega.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/micromega.cmx
 lib/coq/plugins/micromega/micromega_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/micromega/micromega_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/micromega_plugin.o
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/mutils.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/persistent_cache.cmx
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/polynomial.cmx
 lib/coq/plugins/micromega/sos.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/sos.cmx
+${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
 ${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
@@ -619,12 +878,18 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Ns
 lib/coq/plugins/nsatz/Nsatz.glob
 lib/coq/plugins/nsatz/Nsatz.v
 lib/coq/plugins/nsatz/Nsatz.vo
+${PLIST.ocaml-opt}lib/coq/plugins/nsatz/g_nsatz.cmx
 lib/coq/plugins/nsatz/ideal.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/nsatz/ideal.cmx
 lib/coq/plugins/nsatz/nsatz.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/nsatz/nsatz.cmx
 lib/coq/plugins/nsatz/nsatz_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/nsatz/nsatz_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/nsatz/nsatz_plugin.o
 lib/coq/plugins/nsatz/polynom.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/nsatz/polynom.cmx
 lib/coq/plugins/nsatz/utile.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/nsatz/utile.cmx
 ${PLIST.native}lib/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmxs
@@ -660,8 +925,12 @@ lib/coq/plugins/omega/OmegaTactic.vo
 lib/coq/plugins/omega/PreOmega.glob
 lib/coq/plugins/omega/PreOmega.v
 lib/coq/plugins/omega/PreOmega.vo
+${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
 lib/coq/plugins/omega/omega_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/omega/omega_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/omega/omega_plugin.o
 ${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
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmxs
@@ -669,8 +938,11 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/quote/.coq-native/NCoq_quote_Qu
 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.natdynlink}lib/coq/plugins/quote/quote_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/quote/quote_plugin.o
 ${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
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmxs
@@ -686,8 +958,12 @@ 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.natdynlink}lib/coq/plugins/romega/romega_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/romega/romega_plugin.o
 ${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
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmxs
@@ -702,10 +978,14 @@ lib/coq/plugins/rtauto/Bintree.vo
 lib/coq/plugins/rtauto/Rtauto.glob
 lib/coq/plugins/rtauto/Rtauto.v
 lib/coq/plugins/rtauto/Rtauto.vo
+${PLIST.ocaml-opt}lib/coq/plugins/rtauto/g_rtauto.cmx
 lib/coq/plugins/rtauto/proof_search.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/rtauto/proof_search.cmx
 lib/coq/plugins/rtauto/refl_tauto.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/rtauto/refl_tauto.cmx
 lib/coq/plugins/rtauto/rtauto_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/rtauto/rtauto_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/rtauto/rtauto_plugin.o
 ${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
 ${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmxs
@@ -874,10 +1154,13 @@ lib/coq/plugins/setoid_ring/Rings_Z.vo
 lib/coq/plugins/setoid_ring/ZArithRing.glob
 lib/coq/plugins/setoid_ring/ZArithRing.v
 lib/coq/plugins/setoid_ring/ZArithRing.vo
+${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/g_newring.cmx
 lib/coq/plugins/setoid_ring/newring.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/newring.cmx
 lib/coq/plugins/setoid_ring/newring_ast.cmi
 lib/coq/plugins/setoid_ring/newring_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/setoid_ring/newring_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/newring_plugin.o
 ${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
@@ -895,142 +1178,256 @@ lib/coq/plugins/ssr/ssrbool.glob
 lib/coq/plugins/ssr/ssrbool.v
 lib/coq/plugins/ssr/ssrbool.vo
 lib/coq/plugins/ssr/ssrbwd.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrbwd.cmx
 lib/coq/plugins/ssr/ssrcommon.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrcommon.cmx
 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
+${PLIST.natdynlink}lib/coq/plugins/ssr/ssreflect_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssreflect_plugin.o
 lib/coq/plugins/ssr/ssrelim.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrelim.cmx
 lib/coq/plugins/ssr/ssrequality.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrequality.cmx
 lib/coq/plugins/ssr/ssrfun.glob
 lib/coq/plugins/ssr/ssrfun.v
 lib/coq/plugins/ssr/ssrfun.vo
 lib/coq/plugins/ssr/ssrfwd.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrfwd.cmx
 lib/coq/plugins/ssr/ssripats.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssripats.cmx
 lib/coq/plugins/ssr/ssrparser.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrparser.cmx
 lib/coq/plugins/ssr/ssrprinters.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrprinters.cmx
 lib/coq/plugins/ssr/ssrtacticals.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrtacticals.cmx
 lib/coq/plugins/ssr/ssrvernac.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrvernac.cmx
 lib/coq/plugins/ssr/ssrview.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssrview.cmx
 ${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
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.o
 lib/coq/plugins/ssrmatching/ssrmatching.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/ssrmatching.cmx
 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.cmxs
+${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.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/int31_syntax.cmx
 lib/coq/plugins/syntax/int31_syntax_plugin.cmi
 ${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/nat_syntax.cmx
 lib/coq/plugins/syntax/nat_syntax_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/nat_syntax_plugin.o
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/r_syntax.cmx
 lib/coq/plugins/syntax/r_syntax_plugin.cmi
 ${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.natdynlink}lib/coq/plugins/syntax/string_syntax_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_syntax_plugin.o
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/z_syntax.cmx
 lib/coq/plugins/syntax/z_syntax_plugin.cmi
 ${PLIST.natdynlink}lib/coq/plugins/syntax/z_syntax_plugin.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/z_syntax_plugin.o
 lib/coq/pretyping/arguments_renaming.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/arguments_renaming.cmx
 lib/coq/pretyping/cases.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/cases.cmx
 lib/coq/pretyping/cbv.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/cbv.cmx
 lib/coq/pretyping/classops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/classops.cmx
 lib/coq/pretyping/coercion.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/coercion.cmx
 lib/coq/pretyping/constr_matching.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/constr_matching.cmx
 lib/coq/pretyping/detyping.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/detyping.cmx
 lib/coq/pretyping/evarconv.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/evarconv.cmx
 lib/coq/pretyping/evardefine.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/evardefine.cmx
 lib/coq/pretyping/evarsolve.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/evarsolve.cmx
 lib/coq/pretyping/find_subterm.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/find_subterm.cmx
 lib/coq/pretyping/glob_ops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/glob_ops.cmx
 lib/coq/pretyping/indrec.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/indrec.cmx
 lib/coq/pretyping/inductiveops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/inductiveops.cmx
 lib/coq/pretyping/locusops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/locusops.cmx
 lib/coq/pretyping/miscops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/miscops.cmx
 lib/coq/pretyping/nativenorm.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/nativenorm.cmx
 lib/coq/pretyping/patternops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/patternops.cmx
 lib/coq/pretyping/pretype_errors.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/pretype_errors.cmx
 ${PLIST.ocaml-opt}lib/coq/pretyping/pretyping.a
 lib/coq/pretyping/pretyping.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/pretyping.cmx
 ${PLIST.ocaml-opt}lib/coq/pretyping/pretyping.cmxa
 lib/coq/pretyping/program.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/program.cmx
 lib/coq/pretyping/recordops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/recordops.cmx
 lib/coq/pretyping/redops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/redops.cmx
 lib/coq/pretyping/reductionops.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/reductionops.cmx
 lib/coq/pretyping/retyping.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/retyping.cmx
 lib/coq/pretyping/tacred.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/tacred.cmx
 lib/coq/pretyping/typeclasses.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/typeclasses.cmx
 lib/coq/pretyping/typeclasses_errors.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/typeclasses_errors.cmx
 lib/coq/pretyping/typing.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/typing.cmx
 lib/coq/pretyping/unification.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/unification.cmx
 lib/coq/pretyping/vnorm.cmi
+${PLIST.ocaml-opt}lib/coq/pretyping/vnorm.cmx
 lib/coq/printing/genprint.cmi
+${PLIST.ocaml-opt}lib/coq/printing/genprint.cmx
 lib/coq/printing/ppconstr.cmi
+${PLIST.ocaml-opt}lib/coq/printing/ppconstr.cmx
 lib/coq/printing/pputils.cmi
+${PLIST.ocaml-opt}lib/coq/printing/pputils.cmx
 lib/coq/printing/ppvernac.cmi
+${PLIST.ocaml-opt}lib/coq/printing/ppvernac.cmx
 lib/coq/printing/prettyp.cmi
+${PLIST.ocaml-opt}lib/coq/printing/prettyp.cmx
 lib/coq/printing/printer.cmi
+${PLIST.ocaml-opt}lib/coq/printing/printer.cmx
 ${PLIST.ocaml-opt}lib/coq/printing/printing.a
 ${PLIST.ocaml-opt}lib/coq/printing/printing.cmxa
 lib/coq/printing/printmod.cmi
+${PLIST.ocaml-opt}lib/coq/printing/printmod.cmx
 lib/coq/proofs/clenv.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/clenv.cmx
 lib/coq/proofs/clenvtac.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/clenvtac.cmx
 lib/coq/proofs/evar_refiner.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/evar_refiner.cmx
 lib/coq/proofs/goal.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/goal.cmx
 lib/coq/proofs/logic.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/logic.cmx
 lib/coq/proofs/miscprint.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/miscprint.cmx
 lib/coq/proofs/pfedit.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/pfedit.cmx
 lib/coq/proofs/proof.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/proof.cmx
 lib/coq/proofs/proof_global.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/proof_global.cmx
 lib/coq/proofs/proof_type.cmi
 lib/coq/proofs/proof_using.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/proof_using.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
+${PLIST.ocaml-opt}lib/coq/proofs/refiner.cmx
 lib/coq/proofs/tacmach.cmi
+${PLIST.ocaml-opt}lib/coq/proofs/tacmach.cmx
 lib/coq/stm/asyncTaskQueue.cmi
+${PLIST.ocaml-opt}lib/coq/stm/asyncTaskQueue.cmx
 lib/coq/stm/coqworkmgrApi.cmi
+${PLIST.ocaml-opt}lib/coq/stm/coqworkmgrApi.cmx
 lib/coq/stm/dag.cmi
+${PLIST.ocaml-opt}lib/coq/stm/dag.cmx
 lib/coq/stm/proofBlockDelimiter.cmi
+${PLIST.ocaml-opt}lib/coq/stm/proofBlockDelimiter.cmx
+${PLIST.ocaml-opt}lib/coq/stm/proofworkertop.cmx
+${PLIST.ocaml-opt}lib/coq/stm/queryworkertop.cmx
 lib/coq/stm/spawned.cmi
+${PLIST.ocaml-opt}lib/coq/stm/spawned.cmx
 ${PLIST.ocaml-opt}lib/coq/stm/stm.a
 lib/coq/stm/stm.cmi
+${PLIST.ocaml-opt}lib/coq/stm/stm.cmx
 ${PLIST.ocaml-opt}lib/coq/stm/stm.cmxa
 lib/coq/stm/tQueue.cmi
+${PLIST.ocaml-opt}lib/coq/stm/tQueue.cmx
+${PLIST.ocaml-opt}lib/coq/stm/tacworkertop.cmx
 lib/coq/stm/vcs.cmi
+${PLIST.ocaml-opt}lib/coq/stm/vcs.cmx
 lib/coq/stm/vernac_classifier.cmi
+${PLIST.ocaml-opt}lib/coq/stm/vernac_classifier.cmx
 lib/coq/stm/vio_checking.cmi
+${PLIST.ocaml-opt}lib/coq/stm/vio_checking.cmx
 lib/coq/stm/workerLoop.cmi
+${PLIST.ocaml-opt}lib/coq/stm/workerLoop.cmx
 lib/coq/stm/workerPool.cmi
+${PLIST.ocaml-opt}lib/coq/stm/workerPool.cmx
 lib/coq/tactics/auto.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/auto.cmx
 lib/coq/tactics/autorewrite.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/autorewrite.cmx
 lib/coq/tactics/btermdn.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/btermdn.cmx
 lib/coq/tactics/class_tactics.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/class_tactics.cmx
 lib/coq/tactics/contradiction.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/contradiction.cmx
 lib/coq/tactics/dn.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/dn.cmx
 lib/coq/tactics/dnet.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/dnet.cmx
 lib/coq/tactics/eauto.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/eauto.cmx
 lib/coq/tactics/elim.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/elim.cmx
 lib/coq/tactics/elimschemes.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/elimschemes.cmx
 lib/coq/tactics/eqdecide.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/eqdecide.cmx
 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/hints.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/hints.cmx
 lib/coq/tactics/hipattern.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/hipattern.cmx
 lib/coq/tactics/ind_tables.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/ind_tables.cmx
 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/tacticals.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/tacticals.cmx
 ${PLIST.ocaml-opt}lib/coq/tactics/tactics.a
 lib/coq/tactics/tactics.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/tactics.cmx
 ${PLIST.ocaml-opt}lib/coq/tactics/tactics.cmxa
 lib/coq/tactics/term_dnet.cmi
+${PLIST.ocaml-opt}lib/coq/tactics/term_dnet.cmx
 ${PLIST.native}lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmi
 ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmx
 ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmxs
@@ -3846,39 +4243,65 @@ 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
+${PLIST.ocaml-opt}lib/coq/toplevel/coqinit.cmx
 lib/coq/toplevel/coqloop.cmi
+${PLIST.ocaml-opt}lib/coq/toplevel/coqloop.cmx
 lib/coq/toplevel/coqtop.cmi
+${PLIST.ocaml-opt}lib/coq/toplevel/coqtop.cmx
 ${PLIST.ocaml-opt}lib/coq/toplevel/toplevel.a
 ${PLIST.ocaml-opt}lib/coq/toplevel/toplevel.cmxa
 lib/coq/toplevel/usage.cmi
+${PLIST.ocaml-opt}lib/coq/toplevel/usage.cmx
 lib/coq/toplevel/vernac.cmi
+${PLIST.ocaml-opt}lib/coq/toplevel/vernac.cmx
 ${PLIST.natdynlink}${PLIST.coqide}lib/coq/toploop/coqidetop.cmxs
 ${PLIST.natdynlink}lib/coq/toploop/proofworkertop.cmxs
 ${PLIST.natdynlink}lib/coq/toploop/queryworkertop.cmxs
 ${PLIST.natdynlink}lib/coq/toploop/tacworkertop.cmxs
 lib/coq/vernac/assumptions.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/assumptions.cmx
 lib/coq/vernac/auto_ind_decl.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/auto_ind_decl.cmx
 lib/coq/vernac/class.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/class.cmx
 lib/coq/vernac/classes.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/classes.cmx
 lib/coq/vernac/command.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/command.cmx
 lib/coq/vernac/declareDef.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/declareDef.cmx
 lib/coq/vernac/discharge.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/discharge.cmx
 lib/coq/vernac/explainErr.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/explainErr.cmx
 lib/coq/vernac/himsg.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/himsg.cmx
 lib/coq/vernac/indschemes.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/indschemes.cmx
 lib/coq/vernac/lemmas.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/lemmas.cmx
 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/mltop.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/mltop.cmx
 lib/coq/vernac/obligations.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/obligations.cmx
 lib/coq/vernac/record.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/record.cmx
 lib/coq/vernac/search.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/search.cmx
 lib/coq/vernac/topfmt.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/topfmt.cmx
 ${PLIST.ocaml-opt}lib/coq/vernac/vernac.a
 ${PLIST.ocaml-opt}lib/coq/vernac/vernac.cmxa
 lib/coq/vernac/vernacentries.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/vernacentries.cmx
 lib/coq/vernac/vernacinterp.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/vernacinterp.cmx
 lib/coq/vernac/vernacprop.cmi
+${PLIST.ocaml-opt}lib/coq/vernac/vernacprop.cmx
 man/man1/coq-tex.1
 man/man1/coq_makefile.1
 man/man1/coqc.1
@@ -3896,56 +4319,60 @@ ${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
+share/coq/index_urls.txt
+${PLIST.doc}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
 ${PLIST.doc}share/doc/coq/html/faq/axioms.png
 ${PLIST.doc}share/doc/coq/html/faq/index.html
 ${PLIST.doc}share/doc/coq/html/faq/interval_discr.v
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual001.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual002.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual003.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual004.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual005.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual006.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual007.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual008.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual009.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual010.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual011.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual012.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual013.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual014.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual015.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual016.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual017.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual018.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual019.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual020.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual021.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual022.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual023.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual024.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual025.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual026.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual027.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual028.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual029.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual030.html
-${PLIST.doc}share/doc/coq/html/refman/Reference-Manual031.html
+${PLIST.doc}share/doc/coq/html/refman/addendum.html
+${PLIST.doc}share/doc/coq/html/refman/async-proofs.html
 ${PLIST.doc}share/doc/coq/html/refman/biblio.html
+${PLIST.doc}share/doc/coq/html/refman/canonical-structures.html
+${PLIST.doc}share/doc/coq/html/refman/cases.html
+${PLIST.doc}share/doc/coq/html/refman/cic.html
+${PLIST.doc}share/doc/coq/html/refman/coercions.html
 ${PLIST.doc}share/doc/coq/html/refman/command-index.html
+${PLIST.doc}share/doc/coq/html/refman/commands.html
 ${PLIST.doc}share/doc/coq/html/refman/coqide-queries.png
+${PLIST.doc}share/doc/coq/html/refman/coqide.html
 ${PLIST.doc}share/doc/coq/html/refman/coqide.png
+${PLIST.doc}share/doc/coq/html/refman/credits.html
 ${PLIST.doc}share/doc/coq/html/refman/error-index.html
+${PLIST.doc}share/doc/coq/html/refman/extraction.html
+${PLIST.doc}share/doc/coq/html/refman/gallina-ext.html
+${PLIST.doc}share/doc/coq/html/refman/gallina.html
 ${PLIST.doc}share/doc/coq/html/refman/general-index.html
 ${PLIST.doc}share/doc/coq/html/refman/hevea.css
 ${PLIST.doc}share/doc/coq/html/refman/index.html
 ${PLIST.doc}share/doc/coq/html/refman/index_urls.txt
+${PLIST.doc}share/doc/coq/html/refman/introduction.html
+${PLIST.doc}share/doc/coq/html/refman/ltac.html
+${PLIST.doc}share/doc/coq/html/refman/micromega.html
+${PLIST.doc}share/doc/coq/html/refman/miscellaneous.html
+${PLIST.doc}share/doc/coq/html/refman/modules.html
+${PLIST.doc}share/doc/coq/html/refman/nsatz.html
+${PLIST.doc}share/doc/coq/html/refman/omega.html
+${PLIST.doc}share/doc/coq/html/refman/option-index.html
+${PLIST.doc}share/doc/coq/html/refman/program.html
+${PLIST.doc}share/doc/coq/html/refman/proof-handling.html
+${PLIST.doc}share/doc/coq/html/refman/ring.html
+${PLIST.doc}share/doc/coq/html/refman/schemes.html
+${PLIST.doc}share/doc/coq/html/refman/setoid.html
+${PLIST.doc}share/doc/coq/html/refman/ssreflect.html
+${PLIST.doc}share/doc/coq/html/refman/stdlib.html
 ${PLIST.doc}share/doc/coq/html/refman/style.css
+${PLIST.doc}share/doc/coq/html/refman/syntax-extensions.html
+${PLIST.doc}share/doc/coq/html/refman/tactic-examples.html
 ${PLIST.doc}share/doc/coq/html/refman/tactic-index.html
+${PLIST.doc}share/doc/coq/html/refman/tactics.html
 ${PLIST.doc}share/doc/coq/html/refman/toc.html
+${PLIST.doc}share/doc/coq/html/refman/tools.html
+${PLIST.doc}share/doc/coq/html/refman/type-classes.html
+${PLIST.doc}share/doc/coq/html/refman/universes.html
+${PLIST.doc}share/doc/coq/html/refman/vernacular.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Arith.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Arith_base.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Between.html
@@ -3964,6 +4391,7 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Max.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Min.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Minus.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Mult.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.PeanoNat.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Peano_dec.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Plus.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Arith.Wf_nat.html
@@ -3974,6 +4402,10 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Bool.DecBool.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Bool.IfProp.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Bool.Sumbool.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Bool.Zerob.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.CEquivalence.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.CMorphisms.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.CRelationClasses.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.DecidableClass.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.EquivDec.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.Equivalence.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.Init.html
@@ -3985,6 +4417,9 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.RelationPairs.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.SetoidClass.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.SetoidDec.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Classes.SetoidTactics.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Compat.AdmitAxiom.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Compat.Coq85.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Compat.Coq86.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.FSets.FMapAVL.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.FSets.FMapFacts.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.FSets.FMapFullAVL.html
@@ -4009,13 +4444,16 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.FSets.FSets.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Datatypes.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Logic.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Logic_Type.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Nat.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Notations.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Peano.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Prelude.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Specif.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Tactics.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Tauto.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Init.Wf.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Lists.List.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Lists.ListDec.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Lists.ListSet.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Lists.ListTactics.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Lists.SetoidList.html
@@ -4030,10 +4468,8 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ClassicalDescription.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ClassicalEpsilon.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ClassicalFacts.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ClassicalUniqueChoice.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Classical_Pred_Set.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Classical_Pred_Type.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Classical_Prop.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Classical_Type.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ConstructiveEpsilon.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Decidable.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Description.html
@@ -4042,14 +4478,23 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Epsilon.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Eqdep.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.EqdepFacts.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Eqdep_dec.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ExtensionalFunctionRepresentative.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ExtensionalityFacts.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.FinFun.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.FunctionalExtensionality.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.Hurkens.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.IndefiniteDescription.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.JMeq.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ProofIrrelevance.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.ProofIrrelevanceFacts.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.PropExtensionality.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.PropExtensionalityFacts.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.PropFacts.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.RelationalChoice.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.SetIsType.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.SetoidChoice.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.WKL.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Logic.WeakFan.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.MSets.MSetAVL.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.MSets.MSetDecide.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.MSets.MSetEqProperties.html
@@ -4073,20 +4518,10 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.NArith.Ndiv_def.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.NArith.Ngcd_def.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.NArith.Nnat.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.NArith.Nsqrt_def.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.BigNumPrelude.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.BinNums.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.Abstract.CyclicAxioms.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.Abstract.DoubleType.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.Abstract.NZCyclic.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleAdd.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleLift.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleMul.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleSqrt.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleSub.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.DoubleCyclic.DoubleType.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.Int31.Cyclic31.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.Int31.Int31.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.Int31.Ring31.html
@@ -4109,12 +4544,8 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Abstract.ZParity.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Abstract.ZPow.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Abstract.ZProperties.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Abstract.ZSgnAbs.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.BigZ.BigZ.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.BigZ.ZMake.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Binary.ZBinary.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.NatPairs.ZNatPairs.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.SpecViaZ.ZSig.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.NaryFunctions.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.NatInt.NZAdd.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.NatInt.NZAddOrder.html
@@ -4152,18 +4583,9 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.Abstract.NProperties.h
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.Abstract.NSqrt.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.Abstract.NStrongRec.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.Abstract.NSub.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.BigN.BigN.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.BigN.NMake.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.BigN.NMake_gen.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.BigN.Nbasic.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.Binary.NBinary.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.Peano.NPeano.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.SpecViaZ.NSig.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Natural.SpecViaZ.NSigNAxioms.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.NumPrelude.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Rational.BigQ.BigQ.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Rational.BigQ.QMake.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Rational.SpecViaQ.QSig.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.PArith.BinPos.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.PArith.BinPosDef.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.PArith.PArith.html
@@ -4182,6 +4604,7 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.QArith.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.QArith_base.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.QOrderedType.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.Qabs.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.Qcabs.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.Qcanon.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.Qfield.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.QArith.Qminmax.html
@@ -4200,7 +4623,6 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.Cos_rel.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.DiscrR.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.Exp_prop.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.Integration.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.LegacyRfield.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.MVT.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.Machin.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Reals.NewtonInt.html
@@ -4308,6 +4730,7 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Unicode.Utf8_core.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Vectors.Fin.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Vectors.Vector.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Vectors.VectorDef.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.Vectors.VectorEq.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Vectors.VectorSpec.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Wellfounded.Disjoint_Union.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Wellfounded.Inclusion.html
@@ -4325,8 +4748,6 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.Wf_Z.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.ZArith.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.ZArith_base.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.ZArith_dec.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.ZOdiv.html
-${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.ZOdiv_def.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.Zabs.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.Zbool.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.Zcompare.html
@@ -4353,6 +4774,87 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.Zquot.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.Zsqrt_compat.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.Zwf.html
 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.ZArith.auxiliary.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.btauto.Algebra.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.btauto.Btauto.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.btauto.Reflect.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.derive.Derive.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellBasic.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellNatInt.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellNatInteger.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellNatNum.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellString.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellZInt.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellZInteger.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrHaskellZNum.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlBasic.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlBigIntConv.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlIntConv.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlNatBigInt.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlNatInt.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlString.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlZBigInt.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.ExtrOcamlZInt.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.extraction.Extraction.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.fourier.Fourier.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.fourier.Fourier_util.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.funind.FunInd.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.funind.Recdef.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.ltac.Ltac.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.Env.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.EnvRing.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.Lia.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.Lqa.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.Lra.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.MExtraction.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.OrderedRing.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.Psatz.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.QMicromega.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.RMicromega.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.Refl.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.RingMicromega.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.Tauto.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.VarMap.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.ZCoeff.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.micromega.ZMicromega.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.nsatz.Nsatz.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.omega.Omega.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.omega.OmegaLemmas.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.omega.OmegaPlugin.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.omega.OmegaTactic.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.omega.PreOmega.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.quote.Quote.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.romega.ROmega.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.romega.ReflOmegaCore.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.rtauto.Bintree.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.rtauto.Rtauto.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Algebra_syntax.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.ArithRing.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.BinList.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Cring.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Field.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Field_tac.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Field_theory.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.InitialRing.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Integral_domain.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.NArithRing.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ncring.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ncring_initial.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ncring_polynom.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ncring_tac.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.RealField.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ring.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ring_base.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ring_polynom.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ring_tac.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Ring_theory.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Rings_Q.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Rings_R.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.Rings_Z.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.setoid_ring.ZArithRing.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.ssr.ssrbool.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.ssr.ssreflect.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.ssr.ssrfun.html
+${PLIST.doc}share/doc/coq/html/stdlib/Coq.ssrmatching.ssrmatching.html
 ${PLIST.doc}share/doc/coq/html/stdlib/coqdoc.css
 ${PLIST.doc}share/doc/coq/html/stdlib/genindex.html
 ${PLIST.doc}share/doc/coq/html/stdlib/index.html
@@ -4786,6 +5288,7 @@ ${PLIST.doc}share/doc/coq/ps/Library.ps
 ${PLIST.doc}share/doc/coq/ps/RecTutorial.ps
 ${PLIST.doc}share/doc/coq/ps/Reference-Manual.ps
 ${PLIST.doc}share/doc/coq/ps/Tutorial.ps
+${PLIST.doc}share/texmf-dist/tex/latex/coq/coqdoc.sty
 share/emacs/site-lisp/coq-font-lock.el
 share/emacs/site-lisp/coq-inferior.el
 share/emacs/site-lisp/gallina-db.el
@@ -4793,3 +5296,4 @@ share/emacs/site-lisp/gallina-syntax.el
 share/emacs/site-lisp/gallina.el
 share/texmf-dist/tex/latex/coq/coqdoc.sty
 @pkgdir lib/coq/user-contrib
+@pkgdir etc/xdg/coq
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 7b96b4ebf83..30d3feec67e 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,9 +1,7 @@
-$NetBSD: distinfo,v 1.28 2017/11/03 11:20:28 jaapb Exp $
+$NetBSD: distinfo,v 1.29 2018/01/10 16:26:53 jaapb Exp $
 
-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 (coq-8.7.1.tar.gz) = ea4c4bbed3dc1a5550bbb7e2923ed751f9ad2be6
+RMD160 (coq-8.7.1.tar.gz) = 405d24ba9f0eda5b72e8bd0ed0778390cc444bf0
+SHA512 (coq-8.7.1.tar.gz) = 43ef086de93bf99f94d74b9827dd16c79f4d24f5dd4332ee53bbd4588941cb602a64672638a3b3a56bfb612e4dbf7b2a3b5fd4921182dabbbe96e4fef07455b5
+Size (coq-8.7.1.tar.gz) = 5671130 bytes
 SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc
-SHA1 (patch-configure.ml) = 8e48a65709234281e3898ebae9041dfc04c7fe7b
-SHA1 (patch-ide_ideutils.ml) = 7fd59bcfc0cf4f65fd7f4e5a0ec95cb694df8417
diff --git a/lang/coq/options.mk b/lang/coq/options.mk
index 6633d802102..dfbf45c4568 100644
--- a/lang/coq/options.mk
+++ b/lang/coq/options.mk
@@ -1,4 +1,4 @@
-# $NetBSD: options.mk,v 1.2 2014/10/10 08:39:08 jaapb Exp $
+# $NetBSD: options.mk,v 1.3 2018/01/10 16:26:53 jaapb Exp $
 
 PKG_OPTIONS_VAR= PKG_OPTIONS.coq
 PKG_SUPPORTED_OPTIONS= doc coqide
@@ -14,13 +14,16 @@ BUILD_DEPENDS+=		tex-latex-bin-[0-9]*:../../print/tex-latex-bin
 BUILD_DEPENDS+=		makeindexk-[0-9]*:../../textproc/makeindexk
 BUILD_DEPENDS+=		dvipsk-[0-9]*:../../print/dvipsk
 BUILD_DEPENDS+=		tex-babel-[0-9]*:../../print/tex-babel
+BUILD_DEPENDS+=		tex-babel-english-[0-9]*:../../print/tex-babel-english
 BUILD_DEPENDS+=		tex-bibtex-[0-9]*:../../print/tex-bibtex
 BUILD_DEPENDS+=		tex-cm-super-[0-9]*:../../fonts/tex-cm-super
 BUILD_DEPENDS+=		tex-comment-[0-9]*:../../print/tex-comment
 BUILD_DEPENDS+=		tex-ec-[0-9]*:../../fonts/tex-ec
 BUILD_DEPENDS+=		tex-eepic-[0-9]*:../../graphics/tex-eepic
 BUILD_DEPENDS+=		tex-fancyhdr-[0-9]*:../../print/tex-fancyhdr
+BUILD_DEPENDS+=		tex-float-[0-9]*:../../print/tex-float
 BUILD_DEPENDS+=		tex-index-[0-9]*:../../print/tex-index
+BUILD_DEPENDS+=		tex-listings-[0-9]*:../../print/tex-listings
 BUILD_DEPENDS+=		tex-moreverb-[0-9]*:../../print/tex-moreverb
 BUILD_DEPENDS+=		tex-multirow-[0-9]*:../../print/tex-multirow
 BUILD_DEPENDS+=		tex-preprint-[0-9]*:../../print/tex-preprint
@@ -29,6 +32,8 @@ BUILD_DEPENDS+=		tex-psnfss-[0-9]*:../../fonts/tex-psnfss
 BUILD_DEPENDS+=		tex-stmaryrd-[0-9]*:../../fonts/tex-stmaryrd
 BUILD_DEPENDS+=		tex-ucs-[0-9]*:../../print/tex-ucs
 BUILD_DEPENDS+=		tex-xcolor-[0-9]*:../../print/tex-xcolor
+BUILD_DEPENDS+=		fig2dev-[0-9]*:../../print/fig2dev
+.include "../../graphics/ImageMagick/buildlink3.mk"
 .else
 CONFIGURE_ARGS+= -with-doc no
 .endif
diff --git a/lang/coq/patches/patch-configure.ml b/lang/coq/patches/patch-configure.ml
deleted file mode 100644
index efffa43af14..00000000000
--- a/lang/coq/patches/patch-configure.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-$NetBSD: patch-configure.ml,v 1.2 2016/12/30 13:23:06 jaapb Exp $
-
-NetBSD uses md5sum too
---- configure.ml.orig	2016-10-25 20:17:16.000000000 +0000
-+++ configure.ml
-@@ -827,7 +827,7 @@ let strip =
- (** * md5sum command *)
- 
- let md5sum =
--  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"]
-+  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"; "NetBSD"]
-   then "md5 -q" else "md5sum"
- 
- 
diff --git a/lang/coq/patches/patch-ide_ideutils.ml b/lang/coq/patches/patch-ide_ideutils.ml
deleted file mode 100644
index 5720dfc4c0a..00000000000
--- a/lang/coq/patches/patch-ide_ideutils.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-$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