CVS commit: pkgsrc/lang/coq

["Jaap Boender" <jaapb%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   jaapb
Date:           Thu Aug  2 12:57:03 UTC 2018

Modified Files:
        pkgsrc/lang/coq: Makefile PLIST distinfo options.mk

Log Message:
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.


To generate a diff of this commit:
cvs rdiff -u -r1.111 -r1.112 pkgsrc/lang/coq/Makefile
cvs rdiff -u -r1.27 -r1.28 pkgsrc/lang/coq/PLIST
cvs rdiff -u -r1.30 -r1.31 pkgsrc/lang/coq/distinfo
cvs rdiff -u -r1.3 -r1.4 pkgsrc/lang/coq/options.mk

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

Modified files:

Index: pkgsrc/lang/coq/Makefile
diff -u pkgsrc/lang/coq/Makefile:1.111 pkgsrc/lang/coq/Makefile:1.112
--- pkgsrc/lang/coq/Makefile:1.111      Fri Jul 20 03:34:17 2018
+++ pkgsrc/lang/coq/Makefile    Thu Aug  2 12:57:03 2018
@@ -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
 

Index: pkgsrc/lang/coq/PLIST
diff -u pkgsrc/lang/coq/PLIST:1.27 pkgsrc/lang/coq/PLIST:1.28
--- pkgsrc/lang/coq/PLIST:1.27  Sat Jun 16 10:25:51 2018
+++ pkgsrc/lang/coq/PLIST       Thu Aug  2 12:57:03 2018
@@ -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/declara
 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/librar
 ${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/extrac
 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/t
 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
 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/.
 ${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/.co
 ${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
 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/
 ${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
 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.l
 ${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/Co
 ${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/Co
 ${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/Co
 ${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/in
 ${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

Index: pkgsrc/lang/coq/distinfo
diff -u pkgsrc/lang/coq/distinfo:1.30 pkgsrc/lang/coq/distinfo:1.31
--- pkgsrc/lang/coq/distinfo:1.30       Mon Apr  9 11:29:23 2018
+++ pkgsrc/lang/coq/distinfo    Thu Aug  2 12:57:03 2018
@@ -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

Index: pkgsrc/lang/coq/options.mk
diff -u pkgsrc/lang/coq/options.mk:1.3 pkgsrc/lang/coq/options.mk:1.4
--- pkgsrc/lang/coq/options.mk:1.3      Wed Jan 10 16:26:53 2018
+++ pkgsrc/lang/coq/options.mk  Thu Aug  2 12:57:03 2018
@@ -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