Update to 8.6. Fix PORTEPOCH accidentally removed in the previous commit.

6 files changed, 152 insertions, 158 deletions

diff --git a/math/coq/Makefile b/math/coq/Makefile
index 146152d35faf..6303a1752909 100644
--- a/math/coq/Makefile
+++ b/math/coq/Makefile
@@ -1,7 +1,8 @@
 # $FreeBSD$
 
 PORTNAME=	coq
-PORTVERSION=	8.5
+PORTVERSION=	8.6
+PORTEPOCH=	3
 CATEGORIES=	math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${PORTVERSION}/files/ \
 		ftp://ftp.stack.nl/pub/users/johans/coq/
@@ -17,7 +18,6 @@ BUILD_DEPENDS=	camlp5:devel/ocaml-camlp5 \
 LIB_DEPENDS=	libfontconfig.so:x11-fonts/fontconfig \
 		libfreetype.so:print/freetype2
 
-COQVERSION=	${PORTVERSION:R}pl${PORTVERSION:E}
 USES=		gmake gettext-runtime
 USE_EMACS=	yes
 USE_GNOME=	atk cairo gdkpixbuf2 glib20 gtk20 gtksourceview2 pango
@@ -28,8 +28,7 @@ CONFIGURE_ARGS=	-prefix ${PREFIX} \
 		-mandir ${PREFIX}/man \
 		-emacslib ${PREFIX}/share/emacs/site-lisp/coq \
 		-usecamlp5 \
-		-byteonly \
-		-makecmd ${MAKE_CMD}
+		-byteonly
 MAKE_ENV=	VERBOSE=1
 ALL_TARGET=	world
 
diff --git a/math/coq/distinfo b/math/coq/distinfo
index 4cddc4dcdbb6..8702e38e0149 100644
--- a/math/coq/distinfo
+++ b/math/coq/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1483174912
-SHA256 (coq-8.5.tar.gz) = 89a92fb8b91e7cb0797d41c87cd13e4b63bee76c32a6dcc3d7c8055ca6a9ae3d
-SIZE (coq-8.5.tar.gz) = 5346653
+TIMESTAMP = 1483223265
+SHA256 (coq-8.6.tar.gz) = 6e3c3cf5c8e2b0b760dc52738e2e849f3a8c630869659ecc0cf41413fcee81df
+SIZE (coq-8.6.tar.gz) = 5538848
diff --git a/math/coq/files/patch-Makefile.build b/math/coq/files/patch-Makefile.build
index c8767447f442..b66ed54c2c10 100644
--- a/math/coq/files/patch-Makefile.build
+++ b/math/coq/files/patch-Makefile.build
@@ -1,29 +1,11 @@
---- Makefile.build.orig	2016-01-20 16:52:18 UTC
+--- Makefile.build.orig	2016-12-08 15:13:52 UTC
 +++ Makefile.build
-@@ -56,7 +56,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES))
+@@ -101,7 +101,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMEC
+ #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
  
- # Variables meant to be modifiable via the command-line of make
- 
--VERBOSE=
-+VERBOSE=1
- NO_RECOMPILE_ML4=
- NO_RECALC_DEPS=
- READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
-@@ -82,7 +82,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U m
- TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
- 
- COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE)
+ COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
 -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 +BOOTCOQC=$(TIMER) env CAML_LD_LIBRARY_PATH=$${PWD}/kernel/byterun $(COQTOPEXE) -boot $(COQOPTS) -compile
  
- # The SHOW and HIDE variables control whether make will echo complete commands 
- # or only abbreviated versions. 
-@@ -704,7 +704,7 @@ install-doc-no:
- .PHONY: install install-doc-all install-doc-no
- 
- #These variables are intended to be set by the caller to make
--#COQINSTALLPREFIX=
-+COQINSTALLPREFIX=${DESTDIR}
- #OLDROOT=
- 
-   # Can be changed for a local installation (to make packages).
+ LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
+ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
diff --git a/math/coq/files/patch-Makefile.install b/math/coq/files/patch-Makefile.install
new file mode 100644
index 000000000000..6597b7133aa0
--- /dev/null
+++ b/math/coq/files/patch-Makefile.install
@@ -0,0 +1,11 @@
+--- Makefile.install.orig	2016-12-08 15:13:52 UTC
++++ Makefile.install
+@@ -29,7 +29,7 @@ install-doc-no:
+ .PHONY: install install-doc-all install-doc-no
+ 
+ #These variables are intended to be set by the caller to make
+-#COQINSTALLPREFIX=
++COQINSTALLPREFIX=${DESTDIR}
+ #OLDROOT=
+ 
+   # Can be changed for a local installation (to make packages).
diff --git a/math/coq/files/patch-configure.ml b/math/coq/files/patch-configure.ml
deleted file mode 100644
index e31ec3317f4f..000000000000
--- a/math/coq/files/patch-configure.ml
+++ /dev/null
@@ -1,11 +0,0 @@
---- configure.ml.orig	2016-01-20 16:52:18 UTC
-+++ configure.ml
-@@ -843,7 +843,7 @@ let strip =
- (** * md5sum command *)
- 
- let md5sum =
--  if arch = "Darwin" then "md5 -q" else "md5sum"
-+  if arch = "FreeBSD" then "md5 -q" else "md5sum"
- 
- 
- (** * Documentation : do we have latex, hevea, ... *)
diff --git a/math/coq/pkg-plist b/math/coq/pkg-plist
index 5f76d5c0b996..570f31ca5b00 100644
--- a/math/coq/pkg-plist
+++ b/math/coq/pkg-plist
@@ -11,8 +11,22 @@ bin/coqtop.byte
 bin/coqwc
 bin/coqworkmgr
 bin/gallina
+lib/coq/META
 lib/coq/config/coq_config.cmi
 lib/coq/dllcoqrun.so
+lib/coq/engine/engine.cma
+lib/coq/engine/evarutil.cmi
+lib/coq/engine/evd.cmi
+lib/coq/engine/ftactic.cmi
+lib/coq/engine/geninterp.cmi
+lib/coq/engine/logic_monad.cmi
+lib/coq/engine/namegen.cmi
+lib/coq/engine/proofview.cmi
+lib/coq/engine/proofview_monad.cmi
+lib/coq/engine/sigma.cmi
+lib/coq/engine/termops.cmi
+lib/coq/engine/uState.cmi
+lib/coq/grammar/compat5.cmo
 lib/coq/grammar/grammar.cma
 lib/coq/grammar/q_util.cmi
 %%IDE%%lib/coq/ide/config_lexer.cmi
@@ -31,7 +45,9 @@ lib/coq/grammar/q_util.cmi
 %%IDE%%lib/coq/ide/nanoPG.cmi
 %%IDE%%lib/coq/ide/preferences.cmi
 %%IDE%%lib/coq/ide/project_file.cmi
+%%IDE%%lib/coq/ide/richprinter.cmi
 %%IDE%%lib/coq/ide/sentence.cmi
+%%IDE%%lib/coq/ide/serialize.cmi
 %%IDE%%lib/coq/ide/session.cmi
 %%IDE%%lib/coq/ide/tags.cmi
 %%IDE%%lib/coq/ide/utf8_convert.cmi
@@ -52,6 +68,9 @@ lib/coq/grammar/q_util.cmi
 %%IDE%%lib/coq/ide/wg_ProofView.cmi
 %%IDE%%lib/coq/ide/wg_ScriptView.cmi
 %%IDE%%lib/coq/ide/wg_Segment.cmi
+%%IDE%%lib/coq/ide/xml_lexer.cmi
+%%IDE%%lib/coq/ide/xml_parser.cmi
+%%IDE%%lib/coq/ide/xml_printer.cmi
 %%IDE%%lib/coq/ide/xmlprotocol.cmi
 lib/coq/interp/constrarg.cmi
 lib/coq/interp/constrexpr_ops.cmi
@@ -83,10 +102,10 @@ lib/coq/intf/notation_term.cmi
 lib/coq/intf/pattern.cmi
 lib/coq/intf/tacexpr.cmi
 lib/coq/intf/vernacexpr.cmi
+lib/coq/kernel/cClosure.cmi
 lib/coq/kernel/cbytecodes.cmi
 lib/coq/kernel/cbytegen.cmi
 lib/coq/kernel/cemitcodes.cmi
-lib/coq/kernel/closure.cmi
 lib/coq/kernel/constr.cmi
 lib/coq/kernel/context.cmi
 lib/coq/kernel/conv_oracle.cmi
@@ -126,6 +145,7 @@ lib/coq/kernel/term.cmi
 lib/coq/kernel/term_typing.cmi
 lib/coq/kernel/type_errors.cmi
 lib/coq/kernel/typeops.cmi
+lib/coq/kernel/uGraph.cmi
 lib/coq/kernel/uint31.cmi
 lib/coq/kernel/univ.cmi
 lib/coq/kernel/vars.cmi
@@ -135,6 +155,8 @@ lib/coq/lib/aux_file.cmi
 lib/coq/lib/backtrace.cmi
 lib/coq/lib/bigint.cmi
 lib/coq/lib/cArray.cmi
+lib/coq/lib/cEphemeron.cmi
+lib/coq/lib/cErrors.cmi
 lib/coq/lib/cList.cmi
 lib/coq/lib/cMap.cmi
 lib/coq/lib/cObj.cmi
@@ -144,14 +166,13 @@ lib/coq/lib/cStack.cmi
 lib/coq/lib/cString.cmi
 lib/coq/lib/cThread.cmi
 lib/coq/lib/cUnix.cmi
+lib/coq/lib/cWarnings.cmi
 lib/coq/lib/canary.cmi
 lib/coq/lib/clib.cma
 lib/coq/lib/control.cmi
 lib/coq/lib/deque.cmi
 lib/coq/lib/dyn.cmi
 lib/coq/lib/envars.cmi
-lib/coq/lib/ephemeron.cmi
-lib/coq/lib/errors.cmi
 lib/coq/lib/exninfo.cmi
 lib/coq/lib/explore.cmi
 lib/coq/lib/feedback.cmi
@@ -167,6 +188,7 @@ lib/coq/lib/iStream.cmi
 lib/coq/lib/int.cmi
 lib/coq/lib/lib.cma
 lib/coq/lib/loc.cmi
+lib/coq/lib/minisys.cmi
 lib/coq/lib/monad.cmi
 lib/coq/lib/option.cmi
 lib/coq/lib/pp.cmi
@@ -178,7 +200,6 @@ lib/coq/lib/remoteCounter.cmi
 lib/coq/lib/richpp.cmi
 lib/coq/lib/rtree.cmi
 lib/coq/lib/segmenttree.cmi
-lib/coq/lib/serialize.cmi
 lib/coq/lib/spawn.cmi
 lib/coq/lib/stateid.cmi
 lib/coq/lib/store.cmi
@@ -190,9 +211,6 @@ lib/coq/lib/unicodetable.cmi
 lib/coq/lib/unionfind.cmi
 lib/coq/lib/util.cmi
 lib/coq/lib/xml_datatype.cmi
-lib/coq/lib/xml_lexer.cmi
-lib/coq/lib/xml_parser.cmi
-lib/coq/lib/xml_printer.cmi
 lib/coq/library/declare.cmi
 lib/coq/library/declaremods.cmi
 lib/coq/library/decls.cmi
@@ -215,17 +233,39 @@ lib/coq/library/nametab.cmi
 lib/coq/library/states.cmi
 lib/coq/library/summary.cmi
 lib/coq/library/universes.cmi
+lib/coq/ltac/coretactics.cmi
+lib/coq/ltac/evar_tactics.cmi
+lib/coq/ltac/extraargs.cmi
+lib/coq/ltac/extratactics.cmi
+lib/coq/ltac/g_auto.cmi
+lib/coq/ltac/g_class.cmi
+lib/coq/ltac/g_eqdecide.cmi
+lib/coq/ltac/g_ltac.cmi
+lib/coq/ltac/g_obligations.cmi
+lib/coq/ltac/g_rewrite.cmi
+lib/coq/ltac/ltac.cma
+lib/coq/ltac/profile_ltac.cmi
+lib/coq/ltac/profile_ltac_tactics.cmi
+lib/coq/ltac/rewrite.cmi
+lib/coq/ltac/taccoerce.cmi
+lib/coq/ltac/tacentries.cmi
+lib/coq/ltac/tacenv.cmi
+lib/coq/ltac/tacintern.cmi
+lib/coq/ltac/tacinterp.cmi
+lib/coq/ltac/tacsubst.cmi
+lib/coq/ltac/tactic_debug.cmi
+lib/coq/ltac/tactic_option.cmi
+lib/coq/ltac/tauto.cmi
+lib/coq/parsing/cLexer.cmi
 lib/coq/parsing/compat.cmi
 lib/coq/parsing/egramcoq.cmi
 lib/coq/parsing/egramml.cmi
 lib/coq/parsing/g_constr.cmi
-lib/coq/parsing/g_ltac.cmi
 lib/coq/parsing/g_prim.cmi
 lib/coq/parsing/g_proofs.cmi
 lib/coq/parsing/g_tactic.cmi
 lib/coq/parsing/g_vernac.cmi
 lib/coq/parsing/highparsing.cma
-lib/coq/parsing/lexer.cmi
 lib/coq/parsing/parsing.cma
 lib/coq/parsing/pcoq.cmi
 lib/coq/parsing/tok.cmi
@@ -244,23 +284,19 @@ lib/coq/plugins/btauto/Btauto.vo
 lib/coq/plugins/btauto/Reflect.glob
 lib/coq/plugins/btauto/Reflect.v
 lib/coq/plugins/btauto/Reflect.vo
-lib/coq/plugins/btauto/btauto_plugin.cma
-lib/coq/plugins/btauto/btauto_plugin_mod.cmi
-lib/coq/plugins/btauto/g_btauto.cmi
-lib/coq/plugins/btauto/refl_btauto.cmi
-lib/coq/plugins/cc/cc_plugin.cma
-lib/coq/plugins/cc/cc_plugin_mod.cmi
+lib/coq/plugins/btauto/btauto_plugin.cmi
+lib/coq/plugins/btauto/btauto_plugin.cmo
+lib/coq/plugins/cc/cc_plugin.cmi
+lib/coq/plugins/cc/cc_plugin.cmo
 lib/coq/plugins/cc/ccalgo.cmi
 lib/coq/plugins/cc/ccproof.cmi
 lib/coq/plugins/cc/cctac.cmi
-lib/coq/plugins/cc/g_congruence.cmi
 lib/coq/plugins/decl_mode/decl_expr.cmi
 lib/coq/plugins/decl_mode/decl_interp.cmi
 lib/coq/plugins/decl_mode/decl_mode.cmi
-lib/coq/plugins/decl_mode/decl_mode_plugin.cma
-lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
+lib/coq/plugins/decl_mode/decl_mode_plugin.cmi
+lib/coq/plugins/decl_mode/decl_mode_plugin.cmo
 lib/coq/plugins/decl_mode/decl_proof_instr.cmi
-lib/coq/plugins/decl_mode/g_decl_mode.cmi
 lib/coq/plugins/decl_mode/ppdecl_proof.cmi
 lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
 lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmo
@@ -268,8 +304,8 @@ lib/coq/plugins/derive/Derive.glob
 lib/coq/plugins/derive/Derive.v
 lib/coq/plugins/derive/Derive.vo
 lib/coq/plugins/derive/derive.cmi
-lib/coq/plugins/derive/derive_plugin.cma
-lib/coq/plugins/derive/g_derive.cmi
+lib/coq/plugins/derive/derive_plugin.cmi
+lib/coq/plugins/derive/derive_plugin.cmo
 lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi
 lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo
 lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmi
@@ -353,9 +389,8 @@ lib/coq/plugins/extraction/ExtrOcamlZInt.vo
 lib/coq/plugins/extraction/common.cmi
 lib/coq/plugins/extraction/extract_env.cmi
 lib/coq/plugins/extraction/extraction.cmi
-lib/coq/plugins/extraction/extraction_plugin.cma
-lib/coq/plugins/extraction/extraction_plugin_mod.cmi
-lib/coq/plugins/extraction/g_extraction.cmi
+lib/coq/plugins/extraction/extraction_plugin.cmi
+lib/coq/plugins/extraction/extraction_plugin.cmo
 lib/coq/plugins/extraction/haskell.cmi
 lib/coq/plugins/extraction/json.cmi
 lib/coq/plugins/extraction/miniml.cmi
@@ -365,10 +400,9 @@ lib/coq/plugins/extraction/ocaml.cmi
 lib/coq/plugins/extraction/scheme.cmi
 lib/coq/plugins/extraction/table.cmi
 lib/coq/plugins/firstorder/formula.cmi
-lib/coq/plugins/firstorder/g_ground.cmi
 lib/coq/plugins/firstorder/ground.cmi
-lib/coq/plugins/firstorder/ground_plugin.cma
-lib/coq/plugins/firstorder/ground_plugin_mod.cmi
+lib/coq/plugins/firstorder/ground_plugin.cmi
+lib/coq/plugins/firstorder/ground_plugin.cmo
 lib/coq/plugins/firstorder/instances.cmi
 lib/coq/plugins/firstorder/rules.cmi
 lib/coq/plugins/firstorder/sequent.cmi
@@ -383,11 +417,8 @@ lib/coq/plugins/fourier/Fourier.vo
 lib/coq/plugins/fourier/Fourier_util.glob
 lib/coq/plugins/fourier/Fourier_util.v
 lib/coq/plugins/fourier/Fourier_util.vo
-lib/coq/plugins/fourier/fourier.cmi
-lib/coq/plugins/fourier/fourierR.cmi
-lib/coq/plugins/fourier/fourier_plugin.cma
-lib/coq/plugins/fourier/fourier_plugin_mod.cmi
-lib/coq/plugins/fourier/g_fourier.cmi
+lib/coq/plugins/fourier/fourier_plugin.cmi
+lib/coq/plugins/fourier/fourier_plugin.cmo
 lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmi
 lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmo
 lib/coq/plugins/funind/Recdef.glob
@@ -395,22 +426,23 @@ lib/coq/plugins/funind/Recdef.v
 lib/coq/plugins/funind/Recdef.vo
 lib/coq/plugins/funind/functional_principles_proofs.cmi
 lib/coq/plugins/funind/functional_principles_types.cmi
-lib/coq/plugins/funind/g_indfun.cmi
 lib/coq/plugins/funind/glob_term_to_relation.cmi
 lib/coq/plugins/funind/glob_termops.cmi
 lib/coq/plugins/funind/indfun.cmi
 lib/coq/plugins/funind/indfun_common.cmi
-lib/coq/plugins/funind/invfun.cmi
-lib/coq/plugins/funind/merge.cmi
 lib/coq/plugins/funind/recdef.cmi
-lib/coq/plugins/funind/recdef_plugin.cma
-lib/coq/plugins/funind/recdef_plugin_mod.cmi
+lib/coq/plugins/funind/recdef_plugin.cmi
+lib/coq/plugins/funind/recdef_plugin.cmo
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmo
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmo
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmi
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmo
+lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmi
+lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmo
+lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
+lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmo
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmi
@@ -440,6 +472,12 @@ lib/coq/plugins/micromega/EnvRing.vo
 lib/coq/plugins/micromega/Lia.glob
 lib/coq/plugins/micromega/Lia.v
 lib/coq/plugins/micromega/Lia.vo
+lib/coq/plugins/micromega/Lqa.glob
+lib/coq/plugins/micromega/Lqa.v
+lib/coq/plugins/micromega/Lqa.vo
+lib/coq/plugins/micromega/Lra.glob
+lib/coq/plugins/micromega/Lra.v
+lib/coq/plugins/micromega/Lra.vo
 lib/coq/plugins/micromega/OrderedRing.glob
 lib/coq/plugins/micromega/OrderedRing.v
 lib/coq/plugins/micromega/OrderedRing.vo
@@ -470,19 +508,11 @@ lib/coq/plugins/micromega/ZCoeff.vo
 lib/coq/plugins/micromega/ZMicromega.glob
 lib/coq/plugins/micromega/ZMicromega.v
 lib/coq/plugins/micromega/ZMicromega.vo
-lib/coq/plugins/micromega/certificate.cmi
-lib/coq/plugins/micromega/coq_micromega.cmi
 lib/coq/plugins/micromega/csdpcert
-lib/coq/plugins/micromega/g_micromega.cmi
-lib/coq/plugins/micromega/mfourier.cmi
 lib/coq/plugins/micromega/micromega.cmi
-lib/coq/plugins/micromega/micromega_plugin.cma
-lib/coq/plugins/micromega/micromega_plugin_mod.cmi
-lib/coq/plugins/micromega/mutils.cmi
-lib/coq/plugins/micromega/persistent_cache.cmi
-lib/coq/plugins/micromega/polynomial.cmi
+lib/coq/plugins/micromega/micromega_plugin.cmi
+lib/coq/plugins/micromega/micromega_plugin.cmo
 lib/coq/plugins/micromega/sos.cmi
-lib/coq/plugins/micromega/sos_types.cmi
 lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
 lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo
 lib/coq/plugins/nsatz/Nsatz.glob
@@ -490,8 +520,8 @@ lib/coq/plugins/nsatz/Nsatz.v
 lib/coq/plugins/nsatz/Nsatz.vo
 lib/coq/plugins/nsatz/ideal.cmi
 lib/coq/plugins/nsatz/nsatz.cmi
-lib/coq/plugins/nsatz/nsatz_plugin.cma
-lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi
+lib/coq/plugins/nsatz/nsatz_plugin.cmi
+lib/coq/plugins/nsatz/nsatz_plugin.cmo
 lib/coq/plugins/nsatz/polynom.cmi
 lib/coq/plugins/nsatz/utile.cmi
 lib/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmi
@@ -519,20 +549,15 @@ lib/coq/plugins/omega/OmegaTactic.vo
 lib/coq/plugins/omega/PreOmega.glob
 lib/coq/plugins/omega/PreOmega.v
 lib/coq/plugins/omega/PreOmega.vo
-lib/coq/plugins/omega/coq_omega.cmi
-lib/coq/plugins/omega/g_omega.cmi
-lib/coq/plugins/omega/omega.cmi
-lib/coq/plugins/omega/omega_plugin.cma
-lib/coq/plugins/omega/omega_plugin_mod.cmi
+lib/coq/plugins/omega/omega_plugin.cmi
+lib/coq/plugins/omega/omega_plugin.cmo
 lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
 lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmo
 lib/coq/plugins/quote/Quote.glob
 lib/coq/plugins/quote/Quote.v
 lib/coq/plugins/quote/Quote.vo
-lib/coq/plugins/quote/g_quote.cmi
-lib/coq/plugins/quote/quote.cmi
-lib/coq/plugins/quote/quote_plugin.cma
-lib/coq/plugins/quote/quote_plugin_mod.cmi
+lib/coq/plugins/quote/quote_plugin.cmi
+lib/coq/plugins/quote/quote_plugin.cmo
 lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
 lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmo
 lib/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmi
@@ -544,10 +569,8 @@ lib/coq/plugins/romega/ReflOmegaCore.glob
 lib/coq/plugins/romega/ReflOmegaCore.v
 lib/coq/plugins/romega/ReflOmegaCore.vo
 lib/coq/plugins/romega/const_omega.cmi
-lib/coq/plugins/romega/g_romega.cmi
-lib/coq/plugins/romega/refl_omega.cmi
-lib/coq/plugins/romega/romega_plugin.cma
-lib/coq/plugins/romega/romega_plugin_mod.cmi
+lib/coq/plugins/romega/romega_plugin.cmi
+lib/coq/plugins/romega/romega_plugin.cmo
 lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
 lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmo
 lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmi
@@ -558,11 +581,10 @@ lib/coq/plugins/rtauto/Bintree.vo
 lib/coq/plugins/rtauto/Rtauto.glob
 lib/coq/plugins/rtauto/Rtauto.v
 lib/coq/plugins/rtauto/Rtauto.vo
-lib/coq/plugins/rtauto/g_rtauto.cmi
 lib/coq/plugins/rtauto/proof_search.cmi
 lib/coq/plugins/rtauto/refl_tauto.cmi
-lib/coq/plugins/rtauto/rtauto_plugin.cma
-lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi
+lib/coq/plugins/rtauto/rtauto_plugin.cmi
+lib/coq/plugins/rtauto/rtauto_plugin.cmo
 lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
 lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo
 lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmi
@@ -684,26 +706,29 @@ lib/coq/plugins/setoid_ring/ZArithRing.glob
 lib/coq/plugins/setoid_ring/ZArithRing.v
 lib/coq/plugins/setoid_ring/ZArithRing.vo
 lib/coq/plugins/setoid_ring/newring.cmi
-lib/coq/plugins/setoid_ring/newring_plugin.cma
-lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi
-lib/coq/plugins/syntax/ascii_syntax.cmi
-lib/coq/plugins/syntax/ascii_syntax_plugin.cma
-lib/coq/plugins/syntax/ascii_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/nat_syntax.cmi
-lib/coq/plugins/syntax/nat_syntax_plugin.cma
-lib/coq/plugins/syntax/nat_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/numbers_syntax.cmi
-lib/coq/plugins/syntax/numbers_syntax_plugin.cma
-lib/coq/plugins/syntax/numbers_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/r_syntax.cmi
-lib/coq/plugins/syntax/r_syntax_plugin.cma
-lib/coq/plugins/syntax/r_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/string_syntax.cmi
-lib/coq/plugins/syntax/string_syntax_plugin.cma
-lib/coq/plugins/syntax/string_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/z_syntax.cmi
-lib/coq/plugins/syntax/z_syntax_plugin.cma
-lib/coq/plugins/syntax/z_syntax_plugin_mod.cmi
+lib/coq/plugins/setoid_ring/newring_ast.cmi
+lib/coq/plugins/setoid_ring/newring_plugin.cmi
+lib/coq/plugins/setoid_ring/newring_plugin.cmo
+lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
+lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo
+lib/coq/plugins/ssrmatching/ssrmatching.cmi
+lib/coq/plugins/ssrmatching/ssrmatching.glob
+lib/coq/plugins/ssrmatching/ssrmatching.v
+lib/coq/plugins/ssrmatching/ssrmatching.vo
+lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
+lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo
+lib/coq/plugins/syntax/ascii_syntax_plugin.cmi
+lib/coq/plugins/syntax/ascii_syntax_plugin.cmo
+lib/coq/plugins/syntax/nat_syntax_plugin.cmi
+lib/coq/plugins/syntax/nat_syntax_plugin.cmo
+lib/coq/plugins/syntax/numbers_syntax_plugin.cmi
+lib/coq/plugins/syntax/numbers_syntax_plugin.cmo
+lib/coq/plugins/syntax/r_syntax_plugin.cmi
+lib/coq/plugins/syntax/r_syntax_plugin.cmo
+lib/coq/plugins/syntax/string_syntax_plugin.cmi
+lib/coq/plugins/syntax/string_syntax_plugin.cmo
+lib/coq/plugins/syntax/z_syntax_plugin.cmi
+lib/coq/plugins/syntax/z_syntax_plugin.cmo
 lib/coq/pretyping/arguments_renaming.cmi
 lib/coq/pretyping/cases.cmi
 lib/coq/pretyping/cbv.cmi
@@ -712,16 +737,14 @@ lib/coq/pretyping/coercion.cmi
 lib/coq/pretyping/constr_matching.cmi
 lib/coq/pretyping/detyping.cmi
 lib/coq/pretyping/evarconv.cmi
+lib/coq/pretyping/evardefine.cmi
 lib/coq/pretyping/evarsolve.cmi
-lib/coq/pretyping/evarutil.cmi
-lib/coq/pretyping/evd.cmi
 lib/coq/pretyping/find_subterm.cmi
 lib/coq/pretyping/glob_ops.cmi
 lib/coq/pretyping/indrec.cmi
 lib/coq/pretyping/inductiveops.cmi
 lib/coq/pretyping/locusops.cmi
 lib/coq/pretyping/miscops.cmi
-lib/coq/pretyping/namegen.cmi
 lib/coq/pretyping/nativenorm.cmi
 lib/coq/pretyping/patternops.cmi
 lib/coq/pretyping/pretype_errors.cmi
@@ -733,7 +756,6 @@ lib/coq/pretyping/redops.cmi
 lib/coq/pretyping/reductionops.cmi
 lib/coq/pretyping/retyping.cmi
 lib/coq/pretyping/tacred.cmi
-lib/coq/pretyping/termops.cmi
 lib/coq/pretyping/typeclasses.cmi
 lib/coq/pretyping/typeclasses_errors.cmi
 lib/coq/pretyping/typing.cmi
@@ -754,34 +776,30 @@ lib/coq/printing/printer.cmi
 lib/coq/printing/printing.cma
 lib/coq/printing/printmod.cmi
 lib/coq/printing/printmodsig.cmi
-lib/coq/printing/richprinter.cmi
 lib/coq/proofs/clenv.cmi
 lib/coq/proofs/clenvtac.cmi
 lib/coq/proofs/evar_refiner.cmi
 lib/coq/proofs/goal.cmi
 lib/coq/proofs/logic.cmi
-lib/coq/proofs/logic_monad.cmi
 lib/coq/proofs/pfedit.cmi
 lib/coq/proofs/proof.cmi
 lib/coq/proofs/proof_global.cmi
 lib/coq/proofs/proof_type.cmi
 lib/coq/proofs/proof_using.cmi
 lib/coq/proofs/proofs.cma
-lib/coq/proofs/proofview.cmi
-lib/coq/proofs/proofview_monad.cmi
 lib/coq/proofs/redexpr.cmi
+lib/coq/proofs/refine.cmi
 lib/coq/proofs/refiner.cmi
 lib/coq/proofs/tacmach.cmi
-lib/coq/proofs/tactic_debug.cmi
 lib/coq/stm/asyncTaskQueue.cmi
 lib/coq/stm/coqworkmgrApi.cmi
 lib/coq/stm/dag.cmi
 lib/coq/stm/lemmas.cmi
+lib/coq/stm/proofBlockDelimiter.cmi
 lib/coq/stm/spawned.cmi
 lib/coq/stm/stm.cma
 lib/coq/stm/stm.cmi
 lib/coq/stm/tQueue.cmi
-lib/coq/stm/texmacspp.cmi
 lib/coq/stm/vcs.cmi
 lib/coq/stm/vernac_classifier.cmi
 lib/coq/stm/vio_checking.cmi
@@ -791,7 +809,6 @@ lib/coq/tactics/autorewrite.cmi
 lib/coq/tactics/btermdn.cmi
 lib/coq/tactics/class_tactics.cmi
 lib/coq/tactics/contradiction.cmi
-lib/coq/tactics/coretactics.cmi
 lib/coq/tactics/dn.cmi
 lib/coq/tactics/dnet.cmi
 lib/coq/tactics/eauto.cmi
@@ -800,31 +817,14 @@ lib/coq/tactics/elimschemes.cmi
 lib/coq/tactics/eqdecide.cmi
 lib/coq/tactics/eqschemes.cmi
 lib/coq/tactics/equality.cmi
-lib/coq/tactics/evar_tactics.cmi
-lib/coq/tactics/extraargs.cmi
-lib/coq/tactics/extratactics.cmi
-lib/coq/tactics/ftactic.cmi
-lib/coq/tactics/g_class.cmi
-lib/coq/tactics/g_eqdecide.cmi
-lib/coq/tactics/g_rewrite.cmi
-lib/coq/tactics/geninterp.cmi
-lib/coq/tactics/hightactics.cma
 lib/coq/tactics/hints.cmi
 lib/coq/tactics/hipattern.cmi
 lib/coq/tactics/inv.cmi
 lib/coq/tactics/leminv.cmi
-lib/coq/tactics/rewrite.cmi
-lib/coq/tactics/taccoerce.cmi
-lib/coq/tactics/tacenv.cmi
-lib/coq/tactics/tacintern.cmi
-lib/coq/tactics/tacinterp.cmi
-lib/coq/tactics/tacsubst.cmi
 lib/coq/tactics/tactic_matching.cmi
-lib/coq/tactics/tactic_option.cmi
 lib/coq/tactics/tacticals.cmi
 lib/coq/tactics/tactics.cma
 lib/coq/tactics/tactics.cmi
-lib/coq/tactics/tauto.cmi
 lib/coq/tactics/term_dnet.cmi
 lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmi
 lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmo
@@ -1052,6 +1052,8 @@ lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmi
 lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmo
 lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmi
 lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmo
+lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmi
+lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmo
 lib/coq/theories/Compat/AdmitAxiom.glob
 lib/coq/theories/Compat/AdmitAxiom.v
 lib/coq/theories/Compat/AdmitAxiom.vo
@@ -1061,6 +1063,9 @@ lib/coq/theories/Compat/Coq84.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/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
 lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmo
 lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmi
@@ -1184,6 +1189,8 @@ lib/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmi
 lib/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmo
 lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmi
 lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmo
+lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmi
+lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmo
 lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmi
 lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmo
 lib/coq/theories/Init/Datatypes.glob
@@ -1213,6 +1220,9 @@ lib/coq/theories/Init/Specif.vo
 lib/coq/theories/Init/Tactics.glob
 lib/coq/theories/Init/Tactics.v
 lib/coq/theories/Init/Tactics.vo
+lib/coq/theories/Init/Tauto.glob
+lib/coq/theories/Init/Tauto.v
+lib/coq/theories/Init/Tauto.vo
 lib/coq/theories/Init/Wf.glob
 lib/coq/theories/Init/Wf.v
 lib/coq/theories/Init/Wf.vo
@@ -2054,6 +2064,8 @@ lib/coq/theories/QArith/.coq-native/NCoq_QArith_QOrderedType.cmi
 lib/coq/theories/QArith/.coq-native/NCoq_QArith_QOrderedType.cmo
 lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmi
 lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmo
+lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmi
+lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmo
 lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmi
 lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmo
 lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qfield.cmi
@@ -2082,6 +2094,9 @@ lib/coq/theories/QArith/QOrderedType.vo
 lib/coq/theories/QArith/Qabs.glob
 lib/coq/theories/QArith/Qabs.v
 lib/coq/theories/QArith/Qabs.vo
+lib/coq/theories/QArith/Qcabs.glob
+lib/coq/theories/QArith/Qcabs.v
+lib/coq/theories/QArith/Qcabs.vo
 lib/coq/theories/QArith/Qcanon.glob
 lib/coq/theories/QArith/Qcanon.v
 lib/coq/theories/QArith/Qcanon.vo
@@ -2911,12 +2926,10 @@ lib/coq/theories/ZArith/Zwf.vo
 lib/coq/theories/ZArith/auxiliary.glob
 lib/coq/theories/ZArith/auxiliary.v
 lib/coq/theories/ZArith/auxiliary.vo
-lib/coq/tools/compat5.cmo
 lib/coq/tools/coqdoc/coqdoc.css
 lib/coq/tools/coqdoc/coqdoc.sty
 lib/coq/toplevel/assumptions.cmi
 lib/coq/toplevel/auto_ind_decl.cmi
-lib/coq/toplevel/cerrors.cmi
 lib/coq/toplevel/class.cmi
 lib/coq/toplevel/classes.cmi
 lib/coq/toplevel/command.cmi
@@ -2924,7 +2937,7 @@ lib/coq/toplevel/coqinit.cmi
 lib/coq/toplevel/coqloop.cmi
 lib/coq/toplevel/coqtop.cmi
 lib/coq/toplevel/discharge.cmi
-lib/coq/toplevel/g_obligations.cmi
+lib/coq/toplevel/explainErr.cmi
 lib/coq/toplevel/himsg.cmi
 lib/coq/toplevel/ind_tables.cmi
 lib/coq/toplevel/indschemes.cmi