pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/lang/coq
Module Name: pkgsrc
Committed By: jaapb
Date: Wed Jan 10 16:26:53 UTC 2018
Modified Files:
pkgsrc/lang/coq: Makefile PLIST distinfo options.mk
Removed Files:
pkgsrc/lang/coq/patches: patch-configure.ml patch-ide_ideutils.ml
Log Message:
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.
To generate a diff of this commit:
cvs rdiff -u -r1.103 -r1.104 pkgsrc/lang/coq/Makefile
cvs rdiff -u -r1.23 -r1.24 pkgsrc/lang/coq/PLIST
cvs rdiff -u -r1.28 -r1.29 pkgsrc/lang/coq/distinfo
cvs rdiff -u -r1.2 -r1.3 pkgsrc/lang/coq/options.mk
cvs rdiff -u -r1.2 -r0 pkgsrc/lang/coq/patches/patch-configure.ml
cvs rdiff -u -r1.1 -r0 pkgsrc/lang/coq/patches/patch-ide_ideutils.ml
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Modified files:
Index: pkgsrc/lang/coq/Makefile
diff -u pkgsrc/lang/coq/Makefile:1.103 pkgsrc/lang/coq/Makefile:1.104
--- pkgsrc/lang/coq/Makefile:1.103 Thu Nov 30 16:45:28 2017
+++ pkgsrc/lang/coq/Makefile Wed Jan 10 16:26:53 2018
@@ -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 buildlin
SUBST_FILES.fix-paths= config/coq_config.ml
SUBST_SED.fix-paths= -e "s,${BUILDLINK_DIR},${PREFIX},g"
-
.include "../../lang/camlp5/buildlink3.mk"
+.include "../../math/ocaml-num/buildlink3.mk"
.include "../../mk/pthread.buildlink3.mk"
.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/lang/coq/PLIST
diff -u pkgsrc/lang/coq/PLIST:1.23 pkgsrc/lang/coq/PLIST:1.24
--- pkgsrc/lang/coq/PLIST:1.23 Mon Jan 1 22:29:39 2018
+++ pkgsrc/lang/coq/PLIST Wed Jan 10 16:26:53 2018
@@ -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.cm
${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.gl
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
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
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
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.glo
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-fi
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.l
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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/Co
${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
Index: pkgsrc/lang/coq/distinfo
diff -u pkgsrc/lang/coq/distinfo:1.28 pkgsrc/lang/coq/distinfo:1.29
--- pkgsrc/lang/coq/distinfo:1.28 Fri Nov 3 11:20:28 2017
+++ pkgsrc/lang/coq/distinfo Wed Jan 10 16:26:53 2018
@@ -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
Index: pkgsrc/lang/coq/options.mk
diff -u pkgsrc/lang/coq/options.mk:1.2 pkgsrc/lang/coq/options.mk:1.3
--- pkgsrc/lang/coq/options.mk:1.2 Fri Oct 10 08:39:08 2014
+++ pkgsrc/lang/coq/options.mk Wed Jan 10 16:26:53 2018
@@ -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]*:..
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]*:../..
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
Home |
Main Index |
Thread Index |
Old Index