diff options
author | jaapb <jaapb@pkgsrc.org> | 2018-08-02 12:57:03 +0000 |
---|---|---|
committer | jaapb <jaapb@pkgsrc.org> | 2018-08-02 12:57:03 +0000 |
commit | 71e27fd69d4a2dc63a63e1c30db5bd16e33e7f47 (patch) | |
tree | da0d2a074f479736bf4ff036a01303c908365882 /lang/coq | |
parent | e47e089c173289be459dafb8f7ca769938a0dd4e (diff) | |
download | pkgsrc-71e27fd69d4a2dc63a63e1c30db5bd16e33e7f47.tar.gz |
Updated package lang/coq to version 8.8.1.
The list of improvements, additions, bugfixes and so on is quite large;
those interested can refer to the CHANGES file in the distribution.
The reference manual has been fully ported to Sphinx.
Diffstat (limited to 'lang/coq')
-rw-r--r-- | lang/coq/Makefile | 14 | ||||
-rw-r--r-- | lang/coq/PLIST | 551 | ||||
-rw-r--r-- | lang/coq/distinfo | 10 | ||||
-rw-r--r-- | lang/coq/options.mk | 54 |
4 files changed, 437 insertions, 192 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index ceef53bd9dd..3dbd00e475a 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -1,8 +1,7 @@ -# $NetBSD: Makefile,v 1.111 2018/07/20 03:34:17 ryoon Exp $ +# $NetBSD: Makefile,v 1.112 2018/08/02 12:57:03 jaapb Exp $ # -DISTNAME= coq-8.7.2 -PKGREVISION= 4 +DISTNAME= coq-8.8.1 CATEGORIES= lang math MASTER_SITES= ${MASTER_SITE_GITHUB:=coq/} GITHUB_TAG= V${PKGVERSION_NOREV} @@ -55,11 +54,14 @@ PLIST.natdynlink= yes .include "../../lang/python/pyversion.mk" REPLACE_SH= configure install.sh -REPLACE_INTERPRETER+= python +REPLACE_INTERPRETER+= python2 python REPLACE.python.old= python REPLACE.python.new= ${PYTHONBIN} -REPLACE_FILES.python= tools/TimeFileMaker.py \ - tools/make-both-single-timing-files.py \ +REPLACE_FILES.python= tools/TimeFileMaker.py + +REPLACE.python2.old= python2 +REPLACE.python2.new= ${PYTHONBIN} +REPLACE_FILES.python2= tools/make-both-single-timing-files.py \ tools/make-both-time-files.py \ tools/make-one-time-file.py diff --git a/lang/coq/PLIST b/lang/coq/PLIST index 45e748fd769..873df043142 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -1,4 +1,4 @@ -@comment $NetBSD: PLIST,v 1.27 2018/06/16 10:25:51 markd Exp $ +@comment $NetBSD: PLIST,v 1.28 2018/08/02 12:57:03 jaapb Exp $ bin/coq-tex bin/coq_makefile bin/coqc @@ -6,12 +6,82 @@ bin/coqchk bin/coqdep bin/coqdoc ${PLIST.coqide}bin/coqide -bin/coqmktop bin/coqtop bin/coqwc bin/coqworkmgr bin/gallina lib/coq/META +lib/coq/clib/backtrace.cmi +${PLIST.ocaml-opt}lib/coq/clib/backtrace.cmx +lib/coq/clib/bigint.cmi +${PLIST.ocaml-opt}lib/coq/clib/bigint.cmx +lib/coq/clib/cArray.cmi +${PLIST.ocaml-opt}lib/coq/clib/cArray.cmx +lib/coq/clib/cEphemeron.cmi +${PLIST.ocaml-opt}lib/coq/clib/cEphemeron.cmx +lib/coq/clib/cList.cmi +${PLIST.ocaml-opt}lib/coq/clib/cList.cmx +lib/coq/clib/cMap.cmi +${PLIST.ocaml-opt}lib/coq/clib/cMap.cmx +lib/coq/clib/cObj.cmi +${PLIST.ocaml-opt}lib/coq/clib/cObj.cmx +lib/coq/clib/cSet.cmi +${PLIST.ocaml-opt}lib/coq/clib/cSet.cmx +lib/coq/clib/cSig.cmi +lib/coq/clib/cStack.cmi +${PLIST.ocaml-opt}lib/coq/clib/cStack.cmx +lib/coq/clib/cString.cmi +${PLIST.ocaml-opt}lib/coq/clib/cString.cmx +lib/coq/clib/cThread.cmi +${PLIST.ocaml-opt}lib/coq/clib/cThread.cmx +lib/coq/clib/cUnix.cmi +${PLIST.ocaml-opt}lib/coq/clib/cUnix.cmx +lib/coq/clib/canary.cmi +${PLIST.ocaml-opt}lib/coq/clib/canary.cmx +${PLIST.ocaml-opt}lib/coq/clib/clib.a +${PLIST.ocaml-opt}lib/coq/clib/clib.cmxa +lib/coq/clib/dyn.cmi +${PLIST.ocaml-opt}lib/coq/clib/dyn.cmx +lib/coq/clib/exninfo.cmi +${PLIST.ocaml-opt}lib/coq/clib/exninfo.cmx +lib/coq/clib/hMap.cmi +${PLIST.ocaml-opt}lib/coq/clib/hMap.cmx +lib/coq/clib/hashcons.cmi +${PLIST.ocaml-opt}lib/coq/clib/hashcons.cmx +lib/coq/clib/hashset.cmi +${PLIST.ocaml-opt}lib/coq/clib/hashset.cmx +lib/coq/clib/heap.cmi +${PLIST.ocaml-opt}lib/coq/clib/heap.cmx +lib/coq/clib/iStream.cmi +${PLIST.ocaml-opt}lib/coq/clib/iStream.cmx +lib/coq/clib/int.cmi +${PLIST.ocaml-opt}lib/coq/clib/int.cmx +lib/coq/clib/minisys.cmi +${PLIST.ocaml-opt}lib/coq/clib/minisys.cmx +lib/coq/clib/monad.cmi +${PLIST.ocaml-opt}lib/coq/clib/monad.cmx +lib/coq/clib/option.cmi +${PLIST.ocaml-opt}lib/coq/clib/option.cmx +lib/coq/clib/orderedType.cmi +${PLIST.ocaml-opt}lib/coq/clib/orderedType.cmx +lib/coq/clib/predicate.cmi +${PLIST.ocaml-opt}lib/coq/clib/predicate.cmx +lib/coq/clib/range.cmi +${PLIST.ocaml-opt}lib/coq/clib/range.cmx +lib/coq/clib/segmenttree.cmi +${PLIST.ocaml-opt}lib/coq/clib/segmenttree.cmx +lib/coq/clib/store.cmi +${PLIST.ocaml-opt}lib/coq/clib/store.cmx +lib/coq/clib/terminal.cmi +${PLIST.ocaml-opt}lib/coq/clib/terminal.cmx +lib/coq/clib/trie.cmi +${PLIST.ocaml-opt}lib/coq/clib/trie.cmx +lib/coq/clib/unicode.cmi +${PLIST.ocaml-opt}lib/coq/clib/unicode.cmx +lib/coq/clib/unicodetable.cmi +${PLIST.ocaml-opt}lib/coq/clib/unicodetable.cmx +lib/coq/clib/unionfind.cmi +${PLIST.ocaml-opt}lib/coq/clib/unionfind.cmx lib/coq/config/coq_config.cmi ${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx lib/coq/engine/eConstr.cmi @@ -24,12 +94,12 @@ 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/nameops.cmi +${PLIST.ocaml-opt}lib/coq/engine/nameops.cmx lib/coq/engine/proofview.cmi ${PLIST.ocaml-opt}lib/coq/engine/proofview.cmx lib/coq/engine/proofview_monad.cmi @@ -40,6 +110,8 @@ 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/engine/univops.cmi +${PLIST.ocaml-opt}lib/coq/engine/univops.cmx lib/coq/grammar/grammar.cma lib/coq/grammar/q_util.cmi ${PLIST.coqide}lib/coq/ide/config_lexer.cmi @@ -74,6 +146,7 @@ ${PLIST.coqide}lib/coq/ide/wg_Find.cmi ${PLIST.coqide}lib/coq/ide/wg_MessageView.cmi ${PLIST.coqide}lib/coq/ide/wg_Notebook.cmi ${PLIST.coqide}lib/coq/ide/wg_ProofView.cmi +${PLIST.coqide}lib/coq/ide/wg_RoutedMessageViews.cmi ${PLIST.coqide}lib/coq/ide/wg_ScriptView.cmi ${PLIST.coqide}lib/coq/ide/wg_Segment.cmi ${PLIST.coqide}lib/coq/ide/xml_lexer.cmi @@ -88,6 +161,8 @@ 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/discharge.cmi +${PLIST.ocaml-opt}lib/coq/interp/discharge.cmx lib/coq/interp/dumpglob.cmi ${PLIST.ocaml-opt}lib/coq/interp/dumpglob.cmx lib/coq/interp/genintern.cmi @@ -114,6 +189,8 @@ 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/tactypes.cmi +${PLIST.ocaml-opt}lib/coq/interp/tactypes.cmx lib/coq/interp/topconstr.cmi ${PLIST.ocaml-opt}lib/coq/interp/topconstr.cmx lib/coq/intf/constrexpr.cmi @@ -138,20 +215,23 @@ 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 ${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/cPrimitives.cmi +${PLIST.ocaml-opt}lib/coq/kernel/cPrimitives.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/cinstr.cmi +lib/coq/kernel/clambda.cmi +${PLIST.ocaml-opt}lib/coq/kernel/clambda.cmx lib/coq/kernel/constr.cmi ${PLIST.ocaml-opt}lib/coq/kernel/constr.cmx lib/coq/kernel/context.cmi @@ -169,6 +249,7 @@ ${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 +${PLIST.ocaml-opt}lib/coq/kernel/entries.cmx lib/coq/kernel/environ.cmi ${PLIST.ocaml-opt}lib/coq/kernel/environ.cmx lib/coq/kernel/esubst.cmi @@ -206,8 +287,6 @@ 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 @@ -238,55 +317,26 @@ 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/kernel/vmvalues.cmi +${PLIST.ocaml-opt}lib/coq/kernel/vmvalues.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/cProfile.cmi +${PLIST.ocaml-opt}lib/coq/lib/cProfile.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/dAst.cmi +${PLIST.ocaml-opt}lib/coq/lib/dAst.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 @@ -297,60 +347,24 @@ 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 @@ -386,16 +400,12 @@ ${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 @@ -410,8 +420,6 @@ 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 @@ -605,6 +613,7 @@ ${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 +${PLIST.ocaml-opt}lib/coq/plugins/extraction/miniml.cmx lib/coq/plugins/extraction/mlutil.cmi ${PLIST.ocaml-opt}lib/coq/plugins/extraction/mlutil.cmx lib/coq/plugins/extraction/modutil.cmi @@ -680,8 +689,8 @@ 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 +lib/coq/plugins/funind/invfun.cmi ${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 @@ -731,6 +740,7 @@ ${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 +${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacexpr.cmx lib/coq/plugins/ltac/tacintern.cmi ${PLIST.ocaml-opt}lib/coq/plugins/ltac/tacintern.cmx lib/coq/plugins/ltac/tacinterp.cmi @@ -1173,6 +1183,7 @@ ${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 +${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/newring_ast.cmx lib/coq/plugins/setoid_ring/newring_plugin.cmi ${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/newring_plugin.cmx ${PLIST.natdynlink}lib/coq/plugins/setoid_ring/newring_plugin.cmxs @@ -1290,14 +1301,20 @@ 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/geninterp.cmi +${PLIST.ocaml-opt}lib/coq/pretyping/geninterp.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/inferCumulativity.cmi +${PLIST.ocaml-opt}lib/coq/pretyping/inferCumulativity.cmx lib/coq/pretyping/locusops.cmi ${PLIST.ocaml-opt}lib/coq/pretyping/locusops.cmx +lib/coq/pretyping/ltac_pretype.cmi +${PLIST.ocaml-opt}lib/coq/pretyping/ltac_pretype.cmx lib/coq/pretyping/miscops.cmi ${PLIST.ocaml-opt}lib/coq/pretyping/miscops.cmx lib/coq/pretyping/nativenorm.cmi @@ -1330,6 +1347,8 @@ 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/univdecls.cmi +${PLIST.ocaml-opt}lib/coq/pretyping/univdecls.cmx lib/coq/pretyping/vnorm.cmi ${PLIST.ocaml-opt}lib/coq/pretyping/vnorm.cmx lib/coq/printing/genprint.cmi @@ -1364,11 +1383,12 @@ 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_bullet.cmi +${PLIST.ocaml-opt}lib/coq/proofs/proof_bullet.cmx lib/coq/proofs/proof_global.cmi ${PLIST.ocaml-opt}lib/coq/proofs/proof_global.cmx lib/coq/proofs/proof_type.cmi -lib/coq/proofs/proof_using.cmi -${PLIST.ocaml-opt}lib/coq/proofs/proof_using.cmx +${PLIST.ocaml-opt}lib/coq/proofs/proof_type.cmx ${PLIST.ocaml-opt}lib/coq/proofs/proofs.a ${PLIST.ocaml-opt}lib/coq/proofs/proofs.cmxa lib/coq/proofs/redexpr.cmi @@ -1764,23 +1784,30 @@ ${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.o -${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmi -${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmx -${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmxs -${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.o ${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmxs ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.o +${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.o +${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.o lib/coq/theories/Compat/AdmitAxiom.glob lib/coq/theories/Compat/AdmitAxiom.v lib/coq/theories/Compat/AdmitAxiom.vo -lib/coq/theories/Compat/Coq85.glob -lib/coq/theories/Compat/Coq85.v -lib/coq/theories/Compat/Coq85.vo lib/coq/theories/Compat/Coq86.glob lib/coq/theories/Compat/Coq86.v lib/coq/theories/Compat/Coq86.vo +lib/coq/theories/Compat/Coq87.glob +lib/coq/theories/Compat/Coq87.v +lib/coq/theories/Compat/Coq87.vo +lib/coq/theories/Compat/Coq88.glob +lib/coq/theories/Compat/Coq88.v +lib/coq/theories/Compat/Coq88.vo ${PLIST.native}lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmxs @@ -1932,6 +1959,10 @@ ${PLIST.native}lib/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmxs ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.o +${PLIST.native}lib/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Decimal.o ${PLIST.native}lib/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmxs @@ -1975,6 +2006,9 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Wf. lib/coq/theories/Init/Datatypes.glob lib/coq/theories/Init/Datatypes.v lib/coq/theories/Init/Datatypes.vo +lib/coq/theories/Init/Decimal.glob +lib/coq/theories/Init/Decimal.v +lib/coq/theories/Init/Decimal.vo lib/coq/theories/Init/Logic.glob lib/coq/theories/Init/Logic.v lib/coq/theories/Init/Logic.vo @@ -2471,6 +2505,30 @@ ${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmxs ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.o +${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.o +${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.o +${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.o +${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.o +${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.o +${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmi +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmx +${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmxs +${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.o ${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmxs @@ -2531,6 +2589,24 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/ZModulo/.coq-na lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.glob lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.v lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vo +lib/coq/theories/Numbers/DecimalFacts.glob +lib/coq/theories/Numbers/DecimalFacts.v +lib/coq/theories/Numbers/DecimalFacts.vo +lib/coq/theories/Numbers/DecimalN.glob +lib/coq/theories/Numbers/DecimalN.v +lib/coq/theories/Numbers/DecimalN.vo +lib/coq/theories/Numbers/DecimalNat.glob +lib/coq/theories/Numbers/DecimalNat.v +lib/coq/theories/Numbers/DecimalNat.vo +lib/coq/theories/Numbers/DecimalPos.glob +lib/coq/theories/Numbers/DecimalPos.v +lib/coq/theories/Numbers/DecimalPos.vo +lib/coq/theories/Numbers/DecimalString.glob +lib/coq/theories/Numbers/DecimalString.v +lib/coq/theories/Numbers/DecimalString.vo +lib/coq/theories/Numbers/DecimalZ.glob +lib/coq/theories/Numbers/DecimalZ.v +lib/coq/theories/Numbers/DecimalZ.vo ${PLIST.native}lib/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmi ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmx ${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmxs @@ -4266,19 +4342,22 @@ lib/coq/tools/coqdoc/coqdoc.sty lib/coq/tools/make-both-single-timing-files.py lib/coq/tools/make-both-time-files.py lib/coq/tools/make-one-time-file.py +lib/coq/toplevel/coqargs.cmi +${PLIST.ocaml-opt}lib/coq/toplevel/coqargs.cmx 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/coqtop_opt_bin.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/coqidetop.cmxs ${PLIST.natdynlink}lib/coq/toploop/proofworkertop.cmxs ${PLIST.natdynlink}lib/coq/toploop/queryworkertop.cmxs ${PLIST.natdynlink}lib/coq/toploop/tacworkertop.cmxs @@ -4290,12 +4369,18 @@ 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/comAssumption.cmi +${PLIST.ocaml-opt}lib/coq/vernac/comAssumption.cmx +lib/coq/vernac/comDefinition.cmi +${PLIST.ocaml-opt}lib/coq/vernac/comDefinition.cmx +lib/coq/vernac/comFixpoint.cmi +${PLIST.ocaml-opt}lib/coq/vernac/comFixpoint.cmx +lib/coq/vernac/comInductive.cmi +${PLIST.ocaml-opt}lib/coq/vernac/comInductive.cmx +lib/coq/vernac/comProgramFixpoint.cmi +${PLIST.ocaml-opt}lib/coq/vernac/comProgramFixpoint.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 @@ -4312,6 +4397,8 @@ 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/proof_using.cmi +${PLIST.ocaml-opt}lib/coq/vernac/proof_using.cmx lib/coq/vernac/record.cmi ${PLIST.ocaml-opt}lib/coq/vernac/record.cmx lib/coq/vernac/search.cmi @@ -4326,6 +4413,8 @@ 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 +lib/coq/vernac/vernacstate.cmi +${PLIST.ocaml-opt}lib/coq/vernac/vernacstate.cmx man/man1/coq-tex.1 man/man1/coq_makefile.1 man/man1/coqc.1 @@ -4333,7 +4422,6 @@ man/man1/coqchk.1 man/man1/coqdep.1 man/man1/coqdoc.1 man/man1/coqide.1 -man/man1/coqmktop.1 man/man1/coqtop.1 man/man1/coqtop.byte.1 man/man1/coqtop.opt.1 @@ -4343,60 +4431,11 @@ ${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.doc}share/coq/index_urls.txt ${PLIST.coqide}share/doc/coq/FAQ-CoqIde +${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/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 @@ -4442,8 +4481,9 @@ ${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.Compat.Coq87.html +${PLIST.doc}share/doc/coq/html/stdlib/Coq.Compat.Coq88.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 @@ -4466,6 +4506,7 @@ ${PLIST.doc}share/doc/coq/html/stdlib/Coq.FSets.FSetToFiniteSet.html ${PLIST.doc}share/doc/coq/html/stdlib/Coq.FSets.FSetWeakList.html ${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.Decimal.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 @@ -4550,6 +4591,12 @@ ${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 ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Cyclic.ZModulo.ZModulo.html +${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.DecimalFacts.html +${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.DecimalN.html +${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.DecimalNat.html +${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.DecimalPos.html +${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.DecimalString.html +${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.DecimalZ.html ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Abstract.ZAdd.html ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Abstract.ZAddOrder.html ${PLIST.doc}share/doc/coq/html/stdlib/Coq.Numbers.Integer.Abstract.ZAxioms.html @@ -5302,21 +5349,209 @@ ${PLIST.doc}share/doc/coq/html/stdlib/index_variable_X.html ${PLIST.doc}share/doc/coq/html/stdlib/index_variable_Y.html ${PLIST.doc}share/doc/coq/html/stdlib/index_variable_Z.html ${PLIST.doc}share/doc/coq/html/stdlib/index_variable__.html -${PLIST.doc}share/doc/coq/pdf/FAQ.pdf ${PLIST.doc}share/doc/coq/pdf/Library.pdf ${PLIST.doc}share/doc/coq/pdf/RecTutorial.pdf -${PLIST.doc}share/doc/coq/pdf/Reference-Manual.pdf ${PLIST.doc}share/doc/coq/pdf/Tutorial.pdf -${PLIST.doc}share/doc/coq/ps/FAQ.ps ${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 -share/texmf-dist/tex/latex/coq/coqdoc.sty +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/canonical-structures.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/extended-pattern-matching.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/extraction.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/generalized-rewriting.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/implicit-coercions.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/micromega.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/miscellaneous-extensions.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/nsatz.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/omega.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/parallel-proof-processing.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/program.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/ring.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/type-classes.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/addendum/universe-polymorphism.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/coq-cmdindex.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/coq-exnindex.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/coq-optindex.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/coq-tacindex.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/credits.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/environment.pickle +${PLIST.doc}share/doc/coq/sphinx/doctrees/genindex.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/index.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/language/cic.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/language/coq-library.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/language/gallina-extensions.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/language/gallina-specification-language.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/language/module-system.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/practical-tools/coq-commands.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/practical-tools/coqide.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/practical-tools/utilities.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/preamble.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/proof-engine/detailed-tactic-examples.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/proof-engine/ltac.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/proof-engine/proof-handling.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/proof-engine/ssreflect-proof-language.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/proof-engine/tactics.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/proof-engine/vernacular-commands.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/replaces.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/user-extensions/proof-schemes.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/user-extensions/syntax-extensions.doctree +${PLIST.doc}share/doc/coq/sphinx/doctrees/zebibliography.doctree +${PLIST.doc}share/doc/coq/sphinx/html/.buildinfo +${PLIST.doc}share/doc/coq/sphinx/html/_images/coqide-queries.png +${PLIST.doc}share/doc/coq/sphinx/html/_images/coqide.png +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/canonical-structures.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/extended-pattern-matching.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/extraction.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/generalized-rewriting.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/implicit-coercions.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/micromega.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/miscellaneous-extensions.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/nsatz.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/omega.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/parallel-proof-processing.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/program.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/ring.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/type-classes.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/addendum/universe-polymorphism.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/coq-cmdindex.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/coq-exnindex.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/coq-optindex.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/coq-tacindex.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/credits.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/genindex.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/index.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/language/cic.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/language/coq-library.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/language/gallina-extensions.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/language/gallina-specification-language.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/language/module-system.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/practical-tools/coq-commands.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/practical-tools/coqide.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/practical-tools/utilities.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/preamble.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/proof-engine/detailed-tactic-examples.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/proof-engine/ltac.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/proof-engine/proof-handling.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/proof-engine/ssreflect-proof-language.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/proof-engine/tactics.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/proof-engine/vernacular-commands.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/replaces.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/user-extensions/proof-schemes.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/user-extensions/syntax-extensions.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_sources/zebibliography.rst.txt +${PLIST.doc}share/doc/coq/sphinx/html/_static/CoqNotations.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/ajax-loader.gif +${PLIST.doc}share/doc/coq/sphinx/html/_static/ansi-dark.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/ansi.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/basic.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/comment-bright.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/comment-close.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/comment.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/coqdoc.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/coqide-queries.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/coqide.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/coqnotations.sty +${PLIST.doc}share/doc/coq/sphinx/html/_static/css/badge_only.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/css/theme.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/doctools.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/documentation_options.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/down-pressed.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/down.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/file.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bold.eot +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bold.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bold.woff +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bold.woff2 +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bolditalic.eot +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bolditalic.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bolditalic.woff +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-bolditalic.woff2 +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-italic.eot +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-italic.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-italic.woff +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-italic.woff2 +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-regular.eot +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-regular.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-regular.woff +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/Lato/lato-regular.woff2 +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-bold.eot +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-bold.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-bold.woff +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-bold.woff2 +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-regular.eot +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-regular.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-regular.woff +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/RobotoSlab/roboto-slab-v7-regular.woff2 +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/fontawesome-webfont.eot +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/fontawesome-webfont.svg +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/fontawesome-webfont.ttf +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/fontawesome-webfont.woff +${PLIST.doc}share/doc/coq/sphinx/html/_static/fonts/fontawesome-webfont.woff2 +${PLIST.doc}share/doc/coq/sphinx/html/_static/jquery-3.2.1.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/jquery.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/js/modernizr.min.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/js/theme.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/minus.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/notations.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/notations.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/plus.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/pre-text.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/pygments.css +${PLIST.doc}share/doc/coq/sphinx/html/_static/searchtools.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/underscore-1.3.1.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/underscore.js +${PLIST.doc}share/doc/coq/sphinx/html/_static/up-pressed.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/up.png +${PLIST.doc}share/doc/coq/sphinx/html/_static/websupport.js +${PLIST.doc}share/doc/coq/sphinx/html/addendum/canonical-structures.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/extended-pattern-matching.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/extraction.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/generalized-rewriting.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/implicit-coercions.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/micromega.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/miscellaneous-extensions.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/nsatz.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/omega.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/parallel-proof-processing.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/program.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/ring.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/type-classes.html +${PLIST.doc}share/doc/coq/sphinx/html/addendum/universe-polymorphism.html +${PLIST.doc}share/doc/coq/sphinx/html/coq-cmdindex.html +${PLIST.doc}share/doc/coq/sphinx/html/coq-exnindex.html +${PLIST.doc}share/doc/coq/sphinx/html/coq-optindex.html +${PLIST.doc}share/doc/coq/sphinx/html/coq-tacindex.html +${PLIST.doc}share/doc/coq/sphinx/html/credits.html +${PLIST.doc}share/doc/coq/sphinx/html/genindex.html +${PLIST.doc}share/doc/coq/sphinx/html/index.html +${PLIST.doc}share/doc/coq/sphinx/html/language/cic.html +${PLIST.doc}share/doc/coq/sphinx/html/language/coq-library.html +${PLIST.doc}share/doc/coq/sphinx/html/language/gallina-extensions.html +${PLIST.doc}share/doc/coq/sphinx/html/language/gallina-specification-language.html +${PLIST.doc}share/doc/coq/sphinx/html/language/module-system.html +${PLIST.doc}share/doc/coq/sphinx/html/objects.inv +${PLIST.doc}share/doc/coq/sphinx/html/practical-tools/coq-commands.html +${PLIST.doc}share/doc/coq/sphinx/html/practical-tools/coqide.html +${PLIST.doc}share/doc/coq/sphinx/html/practical-tools/utilities.html +${PLIST.doc}share/doc/coq/sphinx/html/preamble.html +${PLIST.doc}share/doc/coq/sphinx/html/proof-engine/detailed-tactic-examples.html +${PLIST.doc}share/doc/coq/sphinx/html/proof-engine/ltac.html +${PLIST.doc}share/doc/coq/sphinx/html/proof-engine/proof-handling.html +${PLIST.doc}share/doc/coq/sphinx/html/proof-engine/ssreflect-proof-language.html +${PLIST.doc}share/doc/coq/sphinx/html/proof-engine/tactics.html +${PLIST.doc}share/doc/coq/sphinx/html/proof-engine/vernacular-commands.html +${PLIST.doc}share/doc/coq/sphinx/html/replaces.html +${PLIST.doc}share/doc/coq/sphinx/html/search.html +${PLIST.doc}share/doc/coq/sphinx/html/searchindex.js +${PLIST.doc}share/doc/coq/sphinx/html/user-extensions/proof-schemes.html +${PLIST.doc}share/doc/coq/sphinx/html/user-extensions/syntax-extensions.html +${PLIST.doc}share/doc/coq/sphinx/html/zebibliography.html share/emacs/site-lisp/coq-font-lock.el -share/emacs/site-lisp/coq-inferior.el share/emacs/site-lisp/gallina-db.el share/emacs/site-lisp/gallina-syntax.el share/emacs/site-lisp/gallina.el +share/emacs/site-lisp/inferior-coq.el +share/texmf-dist/tex/latex/coq/coqdoc.sty @pkgdir lib/coq/user-contrib +@pkgdir lib/coq/dev @pkgdir etc/xdg/coq diff --git a/lang/coq/distinfo b/lang/coq/distinfo index 66bea3a9a3b..9e6e3d1efa5 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,7 +1,7 @@ -$NetBSD: distinfo,v 1.30 2018/04/09 11:29:23 jaapb Exp $ +$NetBSD: distinfo,v 1.31 2018/08/02 12:57:03 jaapb Exp $ -SHA1 (coq-8.7.2.tar.gz) = 0175cc658aa2c93167572a33e9e39fc63f591258 -RMD160 (coq-8.7.2.tar.gz) = 2fd5c59e0143061e4253d68e8839ae3822d7a614 -SHA512 (coq-8.7.2.tar.gz) = 6117ef243c62805996a21952016acaaf21db6d1b539fc813c19c897e100f45cde2bee7c9fb045b269a241b79306c656969ca8051e3212ea2090f6d7c1afad5a8 -Size (coq-8.7.2.tar.gz) = 5754360 bytes +SHA1 (coq-8.8.1.tar.gz) = 7dd5e31f9dd3f80d6dabfb019d1f495244f61999 +RMD160 (coq-8.8.1.tar.gz) = 72b75b1d3a78c1a34b8bac86a0180b8bb677db14 +SHA512 (coq-8.8.1.tar.gz) = 706fdc196ca4b8f27dae834426d926cd7d2c8b215af8cbb2653a0bda088068ed9f492cf8f11d123a1f2166b26f86e91a84765e53beb20172dc530f6dd796d8d4 +Size (coq-8.8.1.tar.gz) = 5934404 bytes SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc diff --git a/lang/coq/options.mk b/lang/coq/options.mk index dfbf45c4568..e8bf1517f12 100644 --- a/lang/coq/options.mk +++ b/lang/coq/options.mk @@ -1,4 +1,4 @@ -# $NetBSD: options.mk,v 1.3 2018/01/10 16:26:53 jaapb Exp $ +# $NetBSD: options.mk,v 1.4 2018/08/02 12:57:03 jaapb Exp $ PKG_OPTIONS_VAR= PKG_OPTIONS.coq PKG_SUPPORTED_OPTIONS= doc coqide @@ -7,33 +7,41 @@ PKG_SUGGESTED_OPTIONS= coqide .include "../../mk/bsd.options.mk" .if !empty(PKG_OPTIONS:Mdoc) -DEPENDS+= hevea>=1.10:../../textproc/hevea +BUILD_DEPENDS+= hevea>=1.10:../../textproc/hevea CONFIGURE_ARGS+= -with-doc yes PLIST.doc= yes -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-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-multirow-[0-9]*:../../print/tex-multirow BUILD_DEPENDS+= tex-preprint-[0-9]*:../../print/tex-preprint -BUILD_DEPENDS+= tex-pslatex-[0-9]*:../../print/tex-pslatex -BUILD_DEPENDS+= tex-psnfss-[0-9]*:../../fonts/tex-psnfss -BUILD_DEPENDS+= tex-stmaryrd-[0-9]*:../../fonts/tex-stmaryrd +#BUILD_DEPENDS+= tex-pslatex-[0-9]*:../../print/tex-pslatex +#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" +#BUILD_DEPENDS+= tex-xcolor-[0-9]*:../../print/tex-xcolor +#BUILD_DEPENDS+= fig2dev-[0-9]*:../../print/fig2dev +#.include "../../graphics/ImageMagick/buildlink3.mk" +BUILD_DEPENDS+= py[0-9]*-sphinx-[0-9]*:../../textproc/py-sphinx +BUILD_DEPENDS+= py[0-9]*-sphinx-rtd-theme-[0-9]*:../../textproc/py-sphinx-rtd-theme +BUILD_DEPENDS+= py[0-9]*-sphinxcontrib-bibtex-[0-9]*:../../textproc/py-sphinxcontrib-bibtex +BUILD_DEPENDS+= py[0-9]*-pybtex-[0-9]*:../../textproc/py-pybtex +BUILD_DEPENDS+= py[0-9]*-pybtex-docutils-[0-9]*:../../textproc/py-pybtex-docutils +BUILD_DEPENDS+= py[0-9]*-pexpect-[0-9]*:../../devel/py-pexpect +BUILD_DEPENDS+= py[0-9]*-antlr4-[0-9]*:../../textproc/py-antlr4 +BUILD_DEPENDS+= py[0-9]*-beautifulsoup4-[0-9]*:../../www/py-beautifulsoup4 .else CONFIGURE_ARGS+= -with-doc no .endif |