diff options
author | jaapb <jaapb@pkgsrc.org> | 2018-01-10 16:26:53 +0000 |
---|---|---|
committer | jaapb <jaapb@pkgsrc.org> | 2018-01-10 16:26:53 +0000 |
commit | 7279512cad0cf94b22520f5b5c4befd62fa97b3c (patch) | |
tree | e02503c253baf3dff8446ae480a7736d3c4a8659 /lang/coq | |
parent | 3b928f9651d66ddd66a7a828d7b88d5c8fb86f8a (diff) | |
download | pkgsrc-7279512cad0cf94b22520f5b5c4befd62fa97b3c.tar.gz |
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.
Diffstat (limited to 'lang/coq')
-rw-r--r-- | lang/coq/Makefile | 7 | ||||
-rw-r--r-- | lang/coq/PLIST | 642 | ||||
-rw-r--r-- | lang/coq/distinfo | 12 | ||||
-rw-r--r-- | lang/coq/options.mk | 7 | ||||
-rw-r--r-- | lang/coq/patches/patch-configure.ml | 14 | ||||
-rw-r--r-- | lang/coq/patches/patch-ide_ideutils.ml | 14 |
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 |