On Fri, Aug 30, 2019 at 10:01:59AM +0200, Christopher Zimmermann wrote:
> Hi,
>
> I'd like to update math/coq to 8.10+beta2. Which is needed to support
> OCaml 4.08. The only user of coq is lang/compcert and was already
> updated to support Coq 8.10 and OCaml 4.08.
> When this update and the devel/frama-c update are committed the OCaml
> 4.08 update can go in. Tested on amd64 with and without nativecode. OKs?
>
> Christopher
>
Not a coq user, so I can't say if this impacts any use case. But
certainly no objections. Especially since this moves the port even
ahead of what is available in opam!
And I would love to see 4.08 make 6.6.
.... Ken
>
> Index: Makefile
> ===================================================================
> RCS file: /cvs/ports/math/coq/Makefile,v
> retrieving revision 1.40
> diff -u -p -r1.40 Makefile
> --- Makefile 12 Jul 2019 20:47:40 -0000 1.40
> +++ Makefile 30 Aug 2019 07:57:23 -0000
> @@ -2,12 +2,12 @@
>
> COMMENT= proof assistant based on a typed lambda calculus
>
> -V= 8.8.0
> +V= 8.10+beta2
> GH_ACCOUNT = coq
> GH_PROJECT = coq
> GH_TAGNAME = V${V}
> -DISTNAME = ${GH_PROJECT}-${V}
> -WRKDIST = ${WRKDIR}/${GH_PROJECT}-${V}
> +DISTNAME = ${GH_PROJECT}-${V:S/+//}
> +WRKDIST = ${WRKDIR}/${GH_PROJECT}-${V:S/+/-/}
>
> CATEGORIES= math
> HOMEPAGE= https://coq.inria.fr/
> @@ -17,27 +17,23 @@ MAINTAINER= Yozo Toda <y...@v007.vaio.n
> # LGPL 2.1
> PERMIT_PACKAGE= Yes
>
> -WANTLIB += X11 Xcomposite Xcursor Xdamage Xext Xfixes Xi Xinerama
> -WANTLIB += Xrandr Xrender atk-1.0 c cairo fontconfig freetype fribidi
> -WANTLIB += gdk-x11-2.0 gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0
> -WANTLIB += gtksourceview-2.0 gtk-x11-2.0 intl m pango-1.0 pangocairo-1.0
> -WANTLIB += pangoft2-1.0 pthread z
> +WANTLIB += atk-1.0 c cairo cairo-gobject fontconfig freetype gdk-3
> +WANTLIB += gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0 gtk-3
> gtksourceview-3.0
> +WANTLIB += intl m pango-1.0 pangocairo-1.0 pthread z
>
> MODULES= lang/ocaml
>
> -BUILD_DEPENDS= x11/lablgtk2 \
> - lang/ocaml-camlp5 \
> +BUILD_DEPENDS= x11/lablgtk3 \
> math/ocaml-num \
> sysutils/findlib
> -RUN_DEPENDS= x11/lablgtk2
> +RUN_DEPENDS= x11/lablgtk3
>
> DESTDIRNAME= COQINSTALLPREFIX
>
> USE_GMAKE= Yes
>
> CONFIGURE_STYLE= simple
> -CONFIGURE_ARGS= -emacslib ${PREFIX}/share/emacs/site-lisp \
> - -prefix ${PREFIX} \
> +CONFIGURE_ARGS= -prefix ${PREFIX} \
> -libdir ${PREFIX}/lib/ocaml/coq \
> -mandir ${PREFIX}/man \
> -configdir ${SYSCONFDIR}/xdg/coq
> @@ -65,7 +61,7 @@ post-install:
> ${INSTALL_DATA_DIR} \
> ${PREFIX}/share/doc/coq/
> ${INSTALL_DATA} \
> - ${WRKDIST}/{LICENSE,CREDITS,CHANGES,CONTRIBUTING.md,README.md} \
> + ${WRKDIST}/{LICENSE,CREDITS,CONTRIBUTING.md,README.md} \
> ${PREFIX}/share/doc/coq/
>
> .include <bsd.port.mk>
> Index: distinfo
> ===================================================================
> RCS file: /cvs/ports/math/coq/distinfo,v
> retrieving revision 1.14
> diff -u -p -r1.14 distinfo
> --- distinfo 4 Mar 2019 12:51:15 -0000 1.14
> +++ distinfo 30 Aug 2019 07:57:23 -0000
> @@ -1,2 +1,2 @@
> -SHA256 (coq-8.8.0.tar.gz) = yvfB055o4OQe2Svh1XyImD+xLtufqVZnpa0tarqYJj0=
> -SIZE (coq-8.8.0.tar.gz) = 5927663
> +SHA256 (coq-8.10beta2.tar.gz) = LIK7Tew3o/+lfuDWQm8OfezMbLM0AA2+Z7DNUV2FUBY=
> +SIZE (coq-8.10beta2.tar.gz) = 6211659
> Index: patches/patch-Makefile_ide
> ===================================================================
> RCS file: /cvs/ports/math/coq/patches/patch-Makefile_ide,v
> retrieving revision 1.1
> diff -u -p -r1.1 patch-Makefile_ide
> --- patches/patch-Makefile_ide 4 Mar 2019 12:51:15 -0000 1.1
> +++ patches/patch-Makefile_ide 30 Aug 2019 07:57:23 -0000
> @@ -3,7 +3,7 @@ $OpenBSD: patch-Makefile_ide,v 1.1 2019/
> Index: Makefile.ide
> --- Makefile.ide.orig
> +++ Makefile.ide
> -@@ -149,7 +149,7 @@ endif
> +@@ -190,7 +190,7 @@ endif
> ifeq ($(HASCOQIDE),no)
> install-coqide-byte: install-ide-toploop-byte
> else
> Index: patches/patch-Makefile_install
> ===================================================================
> RCS file: patches/patch-Makefile_install
> diff -N patches/patch-Makefile_install
> --- patches/patch-Makefile_install 4 Mar 2019 12:51:15 -0000 1.1
> +++ /dev/null 1 Jan 1970 00:00:00 -0000
> @@ -1,19 +0,0 @@
> -$OpenBSD: patch-Makefile_install,v 1.1 2019/03/04 12:51:15 chrisz Exp $
> -
> -Index: Makefile.install
> ---- Makefile.install.orig
> -+++ Makefile.install
> -@@ -110,11 +110,11 @@ install-devfiles:
> - $(MKDIR) $(FULLCOQLIB)
> - $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA)
> - $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) # Regular CMI files
> -+ $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS)
> -+ifeq ($(BEST),opt)
> - $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) # To avoid warning
> 58 "-opaque"
> - $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static
> linking of plugins
> - $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o) # For static
> linking of plugins
> -- $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS)
> --ifeq ($(BEST),opt)
> - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a)
> $(STATICPLUGINS:.cma=.a)
> - endif
> -
> Index: patches/patch-configure_ml
> ===================================================================
> RCS file: /cvs/ports/math/coq/patches/patch-configure_ml,v
> retrieving revision 1.1
> diff -u -p -r1.1 patch-configure_ml
> --- patches/patch-configure_ml 4 Mar 2019 12:51:15 -0000 1.1
> +++ patches/patch-configure_ml 30 Aug 2019 07:57:23 -0000
> @@ -5,7 +5,7 @@ those ticks seem to prevent proper parsi
> Index: configure.ml
> --- configure.ml.orig
> +++ configure.ml
> -@@ -1077,7 +1077,7 @@ let config_runtime () =
> +@@ -940,7 +940,7 @@ let config_runtime () =
> ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"]
> | _ ->
> let ld="CAML_LD_LIBRARY_PATH" in
> Index: pkg/PFRAG.dynlink-native
> ===================================================================
> RCS file: /cvs/ports/math/coq/pkg/PFRAG.dynlink-native,v
> retrieving revision 1.4
> diff -u -p -r1.4 PFRAG.dynlink-native
> --- pkg/PFRAG.dynlink-native 4 Mar 2019 12:51:15 -0000 1.4
> +++ pkg/PFRAG.dynlink-native 30 Aug 2019 07:57:23 -0000
> @@ -25,17 +25,17 @@
> @bin
> lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmxs
> @bin lib/ocaml/coq/plugins/extraction/extraction_plugin.cmxs
> @bin lib/ocaml/coq/plugins/firstorder/ground_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmxs
> -@bin lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmxs
> -@bin lib/ocaml/coq/plugins/fourier/fourier_plugin.cmxs
> @bin lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmxs
> @bin lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmxs
> @bin lib/ocaml/coq/plugins/funind/recdef_plugin.cmxs
> @bin lib/ocaml/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmxs
> @bin lib/ocaml/coq/plugins/ltac/ltac_plugin.cmxs
> @bin lib/ocaml/coq/plugins/ltac/tauto_plugin.cmxs
> +@bin
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmxs
> +@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmxs
> +@bin
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmxs
> @@ -59,11 +59,6 @@
> @bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaTactic.cmxs
> @bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_PreOmega.cmxs
> @bin lib/ocaml/coq/plugins/omega/omega_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmxs
> -@bin lib/ocaml/coq/plugins/quote/quote_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmxs
> -@bin lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmxs
> -@bin lib/ocaml/coq/plugins/romega/romega_plugin.cmxs
> @bin lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmxs
> @bin lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmxs
> @bin lib/ocaml/coq/plugins/rtauto/rtauto_plugin.cmxs
> @@ -98,12 +93,10 @@
> @bin lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmxs
> @bin
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmxs
> @bin lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.cmxs
> +@bin lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmxs
> +@bin lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmxs
> @bin lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/string_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/z_syntax_plugin.cmxs
> +@bin lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmxs
> @bin lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmxs
> @bin lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Arith_base.cmxs
> @bin lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Between.cmxs
> @@ -149,9 +142,9 @@
> @bin lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidDec.cmxs
> @bin
> lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidTactics.cmxs
> @bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs
> -@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmxs
> -@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmxs
> +@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmxs
> @bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmxs
> +@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFullAVL.cmxs
> @@ -173,6 +166,7 @@
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetToFiniteSet.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmxs
> +@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmxs
> @bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmxs
> @bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmxs
> @bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmxs
> @@ -226,6 +220,7 @@
> @bin
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmxs
> +@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmxs
> @bin lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetAVL.cmxs
> @@ -251,6 +246,7 @@
> @bin lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ngcd_def.cmxs
> @bin lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nnat.cmxs
> @bin lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.cmxs
> +@bin
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmxs
> @bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmxs
> @bin
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmxs
> @bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmxs
> @@ -266,6 +262,9 @@
> @bin
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmxs
> @bin
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Int31.cmxs
> @bin
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.cmxs
> +@bin
> lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmxs
> +@bin
> lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmxs
> +@bin
> lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmxs
> @bin
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmxs
> @bin
> lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmxs
> @bin
> lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAddOrder.cmxs
> @@ -409,6 +408,7 @@
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmxs
> +@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmxs
> @@ -449,6 +449,11 @@
> @bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorted.cmxs
> @bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorting.cmxs
> @bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmxs
> +@bin
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmxs
> @bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmxs
> @bin
> lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableType.cmxs
> @bin
> lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableTypeEx.cmxs
> @@ -513,7 +518,3 @@
> @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmxs
> @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmxs
> @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmxs
> -@bin lib/ocaml/coq/toploop/coqidetop.cmxs
> -@bin lib/ocaml/coq/toploop/proofworkertop.cmxs
> -@bin lib/ocaml/coq/toploop/queryworkertop.cmxs
> -@bin lib/ocaml/coq/toploop/tacworkertop.cmxs
> Index: pkg/PFRAG.native
> ===================================================================
> RCS file: /cvs/ports/math/coq/pkg/PFRAG.native,v
> retrieving revision 1.3
> diff -u -p -r1.3 PFRAG.native
> --- pkg/PFRAG.native 4 Mar 2019 12:51:15 -0000 1.3
> +++ pkg/PFRAG.native 30 Aug 2019 07:57:24 -0000
> @@ -1,5 +1,10 @@
> @comment $OpenBSD: PFRAG.native,v 1.3 2019/03/04 12:51:15 chrisz Exp $
> %%dynlink%%
> +@bin bin/coqidetop.opt
> +@bin bin/coqproofworker.opt
> +@bin bin/coqqueryworker.opt
> +@bin bin/coqtacticworker.opt
> +@bin bin/coqtop.opt
> lib/ocaml/coq/clib/backtrace.cmx
> lib/ocaml/coq/clib/bigint.cmx
> lib/ocaml/coq/clib/cArray.cmx
> @@ -12,9 +17,9 @@ lib/ocaml/coq/clib/cStack.cmx
> lib/ocaml/coq/clib/cString.cmx
> lib/ocaml/coq/clib/cThread.cmx
> lib/ocaml/coq/clib/cUnix.cmx
> -lib/ocaml/coq/clib/canary.cmx
> lib/ocaml/coq/clib/clib.a
> lib/ocaml/coq/clib/clib.cmxa
> +lib/ocaml/coq/clib/diff2.cmx
> lib/ocaml/coq/clib/dyn.cmx
> lib/ocaml/coq/clib/exninfo.cmx
> lib/ocaml/coq/clib/hMap.cmx
> @@ -36,10 +41,13 @@ lib/ocaml/coq/clib/trie.cmx
> lib/ocaml/coq/clib/unicode.cmx
> lib/ocaml/coq/clib/unicodetable.cmx
> lib/ocaml/coq/clib/unionfind.cmx
> +lib/ocaml/coq/config/config.a
> +lib/ocaml/coq/config/config.cmxa
> lib/ocaml/coq/config/coq_config.cmx
> lib/ocaml/coq/engine/eConstr.cmx
> lib/ocaml/coq/engine/engine.a
> lib/ocaml/coq/engine/engine.cmxa
> +lib/ocaml/coq/engine/evar_kinds.cmx
> lib/ocaml/coq/engine/evarutil.cmx
> lib/ocaml/coq/engine/evd.cmx
> lib/ocaml/coq/engine/ftactic.cmx
> @@ -50,10 +58,21 @@ lib/ocaml/coq/engine/proofview.cmx
> lib/ocaml/coq/engine/proofview_monad.cmx
> lib/ocaml/coq/engine/termops.cmx
> lib/ocaml/coq/engine/uState.cmx
> -lib/ocaml/coq/engine/universes.cmx
> +lib/ocaml/coq/engine/univGen.cmx
> +lib/ocaml/coq/engine/univMinim.cmx
> +lib/ocaml/coq/engine/univNames.cmx
> +lib/ocaml/coq/engine/univProblem.cmx
> +lib/ocaml/coq/engine/univSubst.cmx
> lib/ocaml/coq/engine/univops.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib.a
> +lib/ocaml/coq/gramlib/.pack/gramlib.cmxa
> +lib/ocaml/coq/gramlib/.pack/gramlib__Gramext.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib__Grammar.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib__Plexing.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib__Ploc.cmx
> lib/ocaml/coq/ide/ide.a
> lib/ocaml/coq/ide/ide.cmxa
> +lib/ocaml/coq/interp/constrexpr.cmx
> lib/ocaml/coq/interp/constrexpr_ops.cmx
> lib/ocaml/coq/interp/constrextern.cmx
> lib/ocaml/coq/interp/constrintern.cmx
> @@ -68,26 +87,12 @@ lib/ocaml/coq/interp/interp.cmxa
> lib/ocaml/coq/interp/modintern.cmx
> lib/ocaml/coq/interp/notation.cmx
> lib/ocaml/coq/interp/notation_ops.cmx
> -lib/ocaml/coq/interp/ppextend.cmx
> +lib/ocaml/coq/interp/notation_term.cmx
> +lib/ocaml/coq/interp/numTok.cmx
> lib/ocaml/coq/interp/reserve.cmx
> lib/ocaml/coq/interp/smartlocate.cmx
> lib/ocaml/coq/interp/stdarg.cmx
> lib/ocaml/coq/interp/syntax_def.cmx
> -lib/ocaml/coq/interp/tactypes.cmx
> -lib/ocaml/coq/interp/topconstr.cmx
> -lib/ocaml/coq/intf/constrexpr.cmx
> -lib/ocaml/coq/intf/decl_kinds.cmx
> -lib/ocaml/coq/intf/evar_kinds.cmx
> -lib/ocaml/coq/intf/extend.cmx
> -lib/ocaml/coq/intf/genredexpr.cmx
> -lib/ocaml/coq/intf/glob_term.cmx
> -lib/ocaml/coq/intf/intf.a
> -lib/ocaml/coq/intf/intf.cmxa
> -lib/ocaml/coq/intf/locus.cmx
> -lib/ocaml/coq/intf/misctypes.cmx
> -lib/ocaml/coq/intf/notation_term.cmx
> -lib/ocaml/coq/intf/pattern.cmx
> -lib/ocaml/coq/intf/vernacexpr.cmx
> lib/ocaml/coq/kernel/cClosure.cmx
> lib/ocaml/coq/kernel/cPrimitives.cmx
> lib/ocaml/coq/kernel/cbytecodes.cmx
> @@ -106,6 +111,7 @@ lib/ocaml/coq/kernel/entries.cmx
> lib/ocaml/coq/kernel/environ.cmx
> lib/ocaml/coq/kernel/esubst.cmx
> lib/ocaml/coq/kernel/evar.cmx
> +lib/ocaml/coq/kernel/indTyping.cmx
> lib/ocaml/coq/kernel/indtypes.cmx
> lib/ocaml/coq/kernel/inductive.cmx
> lib/ocaml/coq/kernel/kernel.a
> @@ -121,23 +127,26 @@ lib/ocaml/coq/kernel/nativelib.cmx
> lib/ocaml/coq/kernel/nativelibrary.cmx
> lib/ocaml/coq/kernel/nativevalues.cmx
> lib/ocaml/coq/kernel/opaqueproof.cmx
> -lib/ocaml/coq/kernel/pre_env.cmx
> +lib/ocaml/coq/kernel/primred.cmx
> lib/ocaml/coq/kernel/reduction.cmx
> lib/ocaml/coq/kernel/retroknowledge.cmx
> +lib/ocaml/coq/kernel/retypeops.cmx
> lib/ocaml/coq/kernel/safe_typing.cmx
> lib/ocaml/coq/kernel/sorts.cmx
> lib/ocaml/coq/kernel/subtyping.cmx
> lib/ocaml/coq/kernel/term.cmx
> lib/ocaml/coq/kernel/term_typing.cmx
> +lib/ocaml/coq/kernel/transparentState.cmx
> lib/ocaml/coq/kernel/type_errors.cmx
> lib/ocaml/coq/kernel/typeops.cmx
> lib/ocaml/coq/kernel/uGraph.cmx
> -lib/ocaml/coq/kernel/uint31.cmx
> +lib/ocaml/coq/kernel/uint63.cmx
> lib/ocaml/coq/kernel/univ.cmx
> lib/ocaml/coq/kernel/vars.cmx
> lib/ocaml/coq/kernel/vconv.cmx
> lib/ocaml/coq/kernel/vm.cmx
> lib/ocaml/coq/kernel/vmvalues.cmx
> +lib/ocaml/coq/lib/acyclicGraph.cmx
> lib/ocaml/coq/lib/aux_file.cmx
> lib/ocaml/coq/lib/cAst.cmx
> lib/ocaml/coq/lib/cErrors.cmx
> @@ -157,6 +166,7 @@ lib/ocaml/coq/lib/lib.a
> lib/ocaml/coq/lib/lib.cmxa
> lib/ocaml/coq/lib/loc.cmx
> lib/ocaml/coq/lib/pp.cmx
> +lib/ocaml/coq/lib/pp_diff.cmx
> lib/ocaml/coq/lib/remoteCounter.cmx
> lib/ocaml/coq/lib/rtree.cmx
> lib/ocaml/coq/lib/spawn.cmx
> @@ -164,13 +174,12 @@ lib/ocaml/coq/lib/stateid.cmx
> lib/ocaml/coq/lib/system.cmx
> lib/ocaml/coq/lib/util.cmx
> lib/ocaml/coq/library/coqlib.cmx
> +lib/ocaml/coq/library/decl_kinds.cmx
> lib/ocaml/coq/library/declaremods.cmx
> lib/ocaml/coq/library/decls.cmx
> -lib/ocaml/coq/library/dischargedhypsmap.cmx
> lib/ocaml/coq/library/global.cmx
> lib/ocaml/coq/library/globnames.cmx
> lib/ocaml/coq/library/goptions.cmx
> -lib/ocaml/coq/library/heads.cmx
> lib/ocaml/coq/library/keys.cmx
> lib/ocaml/coq/library/kindops.cmx
> lib/ocaml/coq/library/lib.cmx
> @@ -184,15 +193,15 @@ lib/ocaml/coq/library/nametab.cmx
> lib/ocaml/coq/library/states.cmx
> lib/ocaml/coq/library/summary.cmx
> lib/ocaml/coq/parsing/cLexer.cmx
> -lib/ocaml/coq/parsing/egramcoq.cmx
> -lib/ocaml/coq/parsing/egramml.cmx
> +lib/ocaml/coq/parsing/extend.cmx
> lib/ocaml/coq/parsing/g_constr.cmx
> lib/ocaml/coq/parsing/g_prim.cmx
> -lib/ocaml/coq/parsing/g_proofs.cmx
> -lib/ocaml/coq/parsing/g_vernac.cmx
> +lib/ocaml/coq/parsing/notation_gram.cmx
> +lib/ocaml/coq/parsing/notgram_ops.cmx
> lib/ocaml/coq/parsing/parsing.a
> lib/ocaml/coq/parsing/parsing.cmxa
> lib/ocaml/coq/parsing/pcoq.cmx
> +lib/ocaml/coq/parsing/ppextend.cmx
> lib/ocaml/coq/parsing/tok.cmx
> lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
> lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o
> @@ -273,15 +282,6 @@ lib/ocaml/coq/plugins/firstorder/instanc
> lib/ocaml/coq/plugins/firstorder/rules.cmx
> lib/ocaml/coq/plugins/firstorder/sequent.cmx
> lib/ocaml/coq/plugins/firstorder/unify.cmx
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmx
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.o
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmx
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.o
> -lib/ocaml/coq/plugins/fourier/fourier.cmx
> -lib/ocaml/coq/plugins/fourier/fourierR.cmx
> -lib/ocaml/coq/plugins/fourier/fourier_plugin.cmx
> -lib/ocaml/coq/plugins/fourier/fourier_plugin.o
> -lib/ocaml/coq/plugins/fourier/g_fourier.cmx
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmx
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.o
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmx
> @@ -331,10 +331,16 @@ lib/ocaml/coq/plugins/ltac/tactic_option
> lib/ocaml/coq/plugins/ltac/tauto.cmx
> lib/ocaml/coq/plugins/ltac/tauto_plugin.cmx
> lib/ocaml/coq/plugins/ltac/tauto_plugin.o
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmx
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmx
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.o
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmx
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.o
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmx
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmx
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmx
> @@ -367,6 +373,7 @@ lib/ocaml/coq/plugins/micromega/certific
> lib/ocaml/coq/plugins/micromega/coq_micromega.cmx
> lib/ocaml/coq/plugins/micromega/csdpcert.cmx
> lib/ocaml/coq/plugins/micromega/g_micromega.cmx
> +lib/ocaml/coq/plugins/micromega/itv.cmx
> lib/ocaml/coq/plugins/micromega/mfourier.cmx
> lib/ocaml/coq/plugins/micromega/micromega.cmx
> lib/ocaml/coq/plugins/micromega/micromega_plugin.cmx
> @@ -374,9 +381,11 @@ lib/ocaml/coq/plugins/micromega/micromeg
> lib/ocaml/coq/plugins/micromega/mutils.cmx
> lib/ocaml/coq/plugins/micromega/persistent_cache.cmx
> lib/ocaml/coq/plugins/micromega/polynomial.cmx
> +lib/ocaml/coq/plugins/micromega/simplex.cmx
> lib/ocaml/coq/plugins/micromega/sos.cmx
> lib/ocaml/coq/plugins/micromega/sos_lib.cmx
> lib/ocaml/coq/plugins/micromega/sos_types.cmx
> +lib/ocaml/coq/plugins/micromega/vect.cmx
> lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmx
> lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.o
> lib/ocaml/coq/plugins/nsatz/g_nsatz.cmx
> @@ -401,21 +410,6 @@ lib/ocaml/coq/plugins/omega/g_omega.cmx
> lib/ocaml/coq/plugins/omega/omega.cmx
> lib/ocaml/coq/plugins/omega/omega_plugin.cmx
> lib/ocaml/coq/plugins/omega/omega_plugin.o
> -lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmx
> -lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.o
> -lib/ocaml/coq/plugins/quote/g_quote.cmx
> -lib/ocaml/coq/plugins/quote/quote.cmx
> -lib/ocaml/coq/plugins/quote/quote_plugin.cmx
> -lib/ocaml/coq/plugins/quote/quote_plugin.o
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmx
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.o
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmx
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.o
> -lib/ocaml/coq/plugins/romega/const_omega.cmx
> -lib/ocaml/coq/plugins/romega/g_romega.cmx
> -lib/ocaml/coq/plugins/romega/refl_omega.cmx
> -lib/ocaml/coq/plugins/romega/romega_plugin.cmx
> -lib/ocaml/coq/plugins/romega/romega_plugin.o
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.o
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmx
> @@ -499,27 +493,24 @@ lib/ocaml/coq/plugins/ssr/ssrvernac.cmx
> lib/ocaml/coq/plugins/ssr/ssrview.cmx
>
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmx
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.o
> +lib/ocaml/coq/plugins/ssrmatching/g_ssrmatching.cmx
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.cmx
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmx
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.o
> -lib/ocaml/coq/plugins/syntax/ascii_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/int31_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/nat_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.o
> +lib/ocaml/coq/plugins/syntax/g_numeral.cmx
> +lib/ocaml/coq/plugins/syntax/g_string.cmx
> +lib/ocaml/coq/plugins/syntax/int63_syntax.cmx
> +lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmx
> +lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.o
> +lib/ocaml/coq/plugins/syntax/numeral.cmx
> +lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmx
> +lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.o
> lib/ocaml/coq/plugins/syntax/r_syntax.cmx
> lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmx
> lib/ocaml/coq/plugins/syntax/r_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/string_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/string_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/string_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/z_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/z_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/z_syntax_plugin.o
> +lib/ocaml/coq/plugins/syntax/string_notation.cmx
> +lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmx
> +lib/ocaml/coq/plugins/syntax/string_notation_plugin.o
> lib/ocaml/coq/pretyping/arguments_renaming.cmx
> lib/ocaml/coq/pretyping/cases.cmx
> lib/ocaml/coq/pretyping/cbv.cmx
> @@ -532,14 +523,18 @@ lib/ocaml/coq/pretyping/evardefine.cmx
> lib/ocaml/coq/pretyping/evarsolve.cmx
> lib/ocaml/coq/pretyping/find_subterm.cmx
> lib/ocaml/coq/pretyping/geninterp.cmx
> +lib/ocaml/coq/pretyping/globEnv.cmx
> lib/ocaml/coq/pretyping/glob_ops.cmx
> +lib/ocaml/coq/pretyping/glob_term.cmx
> +lib/ocaml/coq/pretyping/heads.cmx
> lib/ocaml/coq/pretyping/indrec.cmx
> lib/ocaml/coq/pretyping/inductiveops.cmx
> lib/ocaml/coq/pretyping/inferCumulativity.cmx
> +lib/ocaml/coq/pretyping/locus.cmx
> lib/ocaml/coq/pretyping/locusops.cmx
> lib/ocaml/coq/pretyping/ltac_pretype.cmx
> -lib/ocaml/coq/pretyping/miscops.cmx
> lib/ocaml/coq/pretyping/nativenorm.cmx
> +lib/ocaml/coq/pretyping/pattern.cmx
> lib/ocaml/coq/pretyping/patternops.cmx
> lib/ocaml/coq/pretyping/pretype_errors.cmx
> lib/ocaml/coq/pretyping/pretyping.a
> @@ -547,7 +542,6 @@ lib/ocaml/coq/pretyping/pretyping.cmx
> lib/ocaml/coq/pretyping/pretyping.cmxa
> lib/ocaml/coq/pretyping/program.cmx
> lib/ocaml/coq/pretyping/recordops.cmx
> -lib/ocaml/coq/pretyping/redops.cmx
> lib/ocaml/coq/pretyping/reductionops.cmx
> lib/ocaml/coq/pretyping/retyping.cmx
> lib/ocaml/coq/pretyping/tacred.cmx
> @@ -555,51 +549,47 @@ lib/ocaml/coq/pretyping/typeclasses.cmx
> lib/ocaml/coq/pretyping/typeclasses_errors.cmx
> lib/ocaml/coq/pretyping/typing.cmx
> lib/ocaml/coq/pretyping/unification.cmx
> -lib/ocaml/coq/pretyping/univdecls.cmx
> lib/ocaml/coq/pretyping/vnorm.cmx
> lib/ocaml/coq/printing/genprint.cmx
> lib/ocaml/coq/printing/ppconstr.cmx
> lib/ocaml/coq/printing/pputils.cmx
> -lib/ocaml/coq/printing/ppvernac.cmx
> lib/ocaml/coq/printing/prettyp.cmx
> lib/ocaml/coq/printing/printer.cmx
> lib/ocaml/coq/printing/printing.a
> lib/ocaml/coq/printing/printing.cmxa
> lib/ocaml/coq/printing/printmod.cmx
> +lib/ocaml/coq/printing/proof_diffs.cmx
> lib/ocaml/coq/proofs/clenv.cmx
> lib/ocaml/coq/proofs/clenvtac.cmx
> lib/ocaml/coq/proofs/evar_refiner.cmx
> lib/ocaml/coq/proofs/goal.cmx
> +lib/ocaml/coq/proofs/goal_select.cmx
> lib/ocaml/coq/proofs/logic.cmx
> lib/ocaml/coq/proofs/miscprint.cmx
> lib/ocaml/coq/proofs/pfedit.cmx
> lib/ocaml/coq/proofs/proof.cmx
> lib/ocaml/coq/proofs/proof_bullet.cmx
> lib/ocaml/coq/proofs/proof_global.cmx
> -lib/ocaml/coq/proofs/proof_type.cmx
> lib/ocaml/coq/proofs/proofs.a
> lib/ocaml/coq/proofs/proofs.cmxa
> -lib/ocaml/coq/proofs/redexpr.cmx
> lib/ocaml/coq/proofs/refine.cmx
> lib/ocaml/coq/proofs/refiner.cmx
> lib/ocaml/coq/proofs/tacmach.cmx
> +lib/ocaml/coq/proofs/tactypes.cmx
> lib/ocaml/coq/stm/asyncTaskQueue.cmx
> lib/ocaml/coq/stm/coqworkmgrApi.cmx
> lib/ocaml/coq/stm/dag.cmx
> lib/ocaml/coq/stm/proofBlockDelimiter.cmx
> -lib/ocaml/coq/stm/proofworkertop.cmx
> -lib/ocaml/coq/stm/queryworkertop.cmx
> lib/ocaml/coq/stm/spawned.cmx
> lib/ocaml/coq/stm/stm.a
> lib/ocaml/coq/stm/stm.cmx
> lib/ocaml/coq/stm/stm.cmxa
> lib/ocaml/coq/stm/tQueue.cmx
> -lib/ocaml/coq/stm/tacworkertop.cmx
> lib/ocaml/coq/stm/vcs.cmx
> lib/ocaml/coq/stm/vernac_classifier.cmx
> lib/ocaml/coq/stm/vio_checking.cmx
> -lib/ocaml/coq/stm/workerLoop.cmx
> lib/ocaml/coq/stm/workerPool.cmx
> +lib/ocaml/coq/tactics/abstract.cmx
> lib/ocaml/coq/tactics/auto.cmx
> lib/ocaml/coq/tactics/autorewrite.cmx
> lib/ocaml/coq/tactics/btermdn.cmx
> @@ -613,11 +603,15 @@ lib/ocaml/coq/tactics/elimschemes.cmx
> lib/ocaml/coq/tactics/eqdecide.cmx
> lib/ocaml/coq/tactics/eqschemes.cmx
> lib/ocaml/coq/tactics/equality.cmx
> +lib/ocaml/coq/tactics/genredexpr.cmx
> lib/ocaml/coq/tactics/hints.cmx
> lib/ocaml/coq/tactics/hipattern.cmx
> lib/ocaml/coq/tactics/ind_tables.cmx
> lib/ocaml/coq/tactics/inv.cmx
> lib/ocaml/coq/tactics/leminv.cmx
> +lib/ocaml/coq/tactics/ppred.cmx
> +lib/ocaml/coq/tactics/redexpr.cmx
> +lib/ocaml/coq/tactics/redops.cmx
> lib/ocaml/coq/tactics/tacticals.cmx
> lib/ocaml/coq/tactics/tactics.a
> lib/ocaml/coq/tactics/tactics.cmx
> @@ -713,12 +707,12 @@ lib/ocaml/coq/theories/Classes/.coq-nati
> lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidTactics.o
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.o
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmx
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.o
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmx
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.o
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmx
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.o
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmx
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.o
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmx
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.o
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmx
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.o
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmx
> @@ -761,6 +755,8 @@ lib/ocaml/coq/theories/FSets/.coq-native
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.o
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmx
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.o
> +lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmx
> +lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.o
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmx
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.o
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmx
> @@ -867,6 +863,8 @@ lib/ocaml/coq/theories/Logic/.coq-native
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.o
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmx
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.o
> +lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmx
> +lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.o
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmx
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.o
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmx
> @@ -917,6 +915,8 @@ lib/ocaml/coq/theories/NArith/.coq-nativ
> lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nnat.o
> lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.cmx
> lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.o
> +lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmx
> +lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.o
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmx
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.o
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmx
> @@ -947,6 +947,12 @@ lib/ocaml/coq/theories/Numbers/Cyclic/In
>
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Int31.o
>
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.cmx
>
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.o
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmx
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.o
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmx
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.o
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmx
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.o
>
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmx
>
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.o
>
> lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmx
> @@ -1233,6 +1239,8 @@ lib/ocaml/coq/theories/Reals/.coq-native
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.o
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmx
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.o
> +lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmx
> +lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.o
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmx
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.o
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmx
> @@ -1313,6 +1321,16 @@ lib/ocaml/coq/theories/Sorting/.coq-nati
> lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorting.o
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmx
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.o
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmx
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.o
>
> lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableType.cmx
> @@ -1441,16 +1459,26 @@ lib/ocaml/coq/theories/ZArith/.coq-nativ
> lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
> lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
> lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.o
> +lib/ocaml/coq/topbin/coqc_bin.cmx
> +lib/ocaml/coq/topbin/coqproofworker_bin.cmx
> +lib/ocaml/coq/topbin/coqqueryworker_bin.cmx
> +lib/ocaml/coq/topbin/coqtacticworker_bin.cmx
> +lib/ocaml/coq/topbin/coqtop_bin.cmx
> +lib/ocaml/coq/toplevel/ccompile.cmx
> lib/ocaml/coq/toplevel/coqargs.cmx
> +lib/ocaml/coq/toplevel/coqc.cmx
> +lib/ocaml/coq/toplevel/coqcargs.cmx
> lib/ocaml/coq/toplevel/coqinit.cmx
> lib/ocaml/coq/toplevel/coqloop.cmx
> lib/ocaml/coq/toplevel/coqtop.cmx
> -lib/ocaml/coq/toplevel/coqtop_opt_bin.cmx
> +lib/ocaml/coq/toplevel/g_toplevel.cmx
> lib/ocaml/coq/toplevel/toplevel.a
> lib/ocaml/coq/toplevel/toplevel.cmxa
> lib/ocaml/coq/toplevel/usage.cmx
> lib/ocaml/coq/toplevel/vernac.cmx
> +lib/ocaml/coq/toplevel/workerLoop.cmx
> lib/ocaml/coq/vernac/assumptions.cmx
> +lib/ocaml/coq/vernac/attributes.cmx
> lib/ocaml/coq/vernac/auto_ind_decl.cmx
> lib/ocaml/coq/vernac/class.cmx
> lib/ocaml/coq/vernac/classes.cmx
> @@ -1460,7 +1488,11 @@ lib/ocaml/coq/vernac/comFixpoint.cmx
> lib/ocaml/coq/vernac/comInductive.cmx
> lib/ocaml/coq/vernac/comProgramFixpoint.cmx
> lib/ocaml/coq/vernac/declareDef.cmx
> +lib/ocaml/coq/vernac/egramcoq.cmx
> +lib/ocaml/coq/vernac/egramml.cmx
> lib/ocaml/coq/vernac/explainErr.cmx
> +lib/ocaml/coq/vernac/g_proofs.cmx
> +lib/ocaml/coq/vernac/g_vernac.cmx
> lib/ocaml/coq/vernac/himsg.cmx
> lib/ocaml/coq/vernac/indschemes.cmx
> lib/ocaml/coq/vernac/lemmas.cmx
> @@ -1468,13 +1500,16 @@ lib/ocaml/coq/vernac/locality.cmx
> lib/ocaml/coq/vernac/metasyntax.cmx
> lib/ocaml/coq/vernac/mltop.cmx
> lib/ocaml/coq/vernac/obligations.cmx
> +lib/ocaml/coq/vernac/ppvernac.cmx
> lib/ocaml/coq/vernac/proof_using.cmx
> +lib/ocaml/coq/vernac/pvernac.cmx
> lib/ocaml/coq/vernac/record.cmx
> lib/ocaml/coq/vernac/search.cmx
> lib/ocaml/coq/vernac/topfmt.cmx
> lib/ocaml/coq/vernac/vernac.a
> lib/ocaml/coq/vernac/vernac.cmxa
> lib/ocaml/coq/vernac/vernacentries.cmx
> -lib/ocaml/coq/vernac/vernacinterp.cmx
> +lib/ocaml/coq/vernac/vernacexpr.cmx
> +lib/ocaml/coq/vernac/vernacextend.cmx
> lib/ocaml/coq/vernac/vernacprop.cmx
> lib/ocaml/coq/vernac/vernacstate.cmx
> Index: pkg/PLIST
> ===================================================================
> RCS file: /cvs/ports/math/coq/pkg/PLIST,v
> retrieving revision 1.11
> diff -u -p -r1.11 PLIST
> --- pkg/PLIST 4 Mar 2019 12:51:15 -0000 1.11
> +++ pkg/PLIST 30 Aug 2019 07:57:24 -0000
> @@ -7,11 +7,12 @@
> @bin bin/coqdep
> @bin bin/coqdoc
> @bin bin/coqide
> +@bin bin/coqidetop
> +bin/coqpp
> @bin bin/coqtop
> @comment bin/coqtop.byte
> @bin bin/coqwc
> @bin bin/coqworkmgr
> -@bin bin/gallina
> lib/ocaml/coq/
> lib/ocaml/coq/META
> lib/ocaml/coq/clib/
> @@ -28,7 +29,7 @@ lib/ocaml/coq/clib/cStack.cmi
> lib/ocaml/coq/clib/cString.cmi
> lib/ocaml/coq/clib/cThread.cmi
> lib/ocaml/coq/clib/cUnix.cmi
> -lib/ocaml/coq/clib/canary.cmi
> +lib/ocaml/coq/clib/diff2.cmi
> lib/ocaml/coq/clib/dyn.cmi
> lib/ocaml/coq/clib/exninfo.cmi
> lib/ocaml/coq/clib/hMap.cmi
> @@ -52,10 +53,14 @@ lib/ocaml/coq/clib/unicodetable.cmi
> lib/ocaml/coq/clib/unionfind.cmi
> lib/ocaml/coq/config/
> lib/ocaml/coq/config/coq_config.cmi
> +lib/ocaml/coq/coqpp/
> +lib/ocaml/coq/coqpp/coqpp_ast.cmi
> +lib/ocaml/coq/coqpp/coqpp_parse.cmi
> lib/ocaml/coq/dev/
> @comment lib/ocaml/coq/dllcoqrun.so
> lib/ocaml/coq/engine/
> lib/ocaml/coq/engine/eConstr.cmi
> +lib/ocaml/coq/engine/evar_kinds.cmi
> lib/ocaml/coq/engine/evarutil.cmi
> lib/ocaml/coq/engine/evd.cmi
> lib/ocaml/coq/engine/ftactic.cmi
> @@ -66,13 +71,24 @@ lib/ocaml/coq/engine/proofview.cmi
> lib/ocaml/coq/engine/proofview_monad.cmi
> lib/ocaml/coq/engine/termops.cmi
> lib/ocaml/coq/engine/uState.cmi
> -lib/ocaml/coq/engine/universes.cmi
> +lib/ocaml/coq/engine/univGen.cmi
> +lib/ocaml/coq/engine/univMinim.cmi
> +lib/ocaml/coq/engine/univNames.cmi
> +lib/ocaml/coq/engine/univProblem.cmi
> +lib/ocaml/coq/engine/univSubst.cmi
> lib/ocaml/coq/engine/univops.cmi
> -lib/ocaml/coq/grammar/
> -lib/ocaml/coq/grammar/grammar.cma
> -lib/ocaml/coq/grammar/q_util.cmi
> +lib/ocaml/coq/gramlib/
> +lib/ocaml/coq/gramlib/.pack/
> +lib/ocaml/coq/gramlib/.pack/gramlib.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Gramext.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Grammar.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Plexing.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Ploc.cmi
> lib/ocaml/coq/ide/
> lib/ocaml/coq/ide/config_lexer.cmi
> +lib/ocaml/coq/ide/configwin.cmi
> +lib/ocaml/coq/ide/configwin_ihm.cmi
> +lib/ocaml/coq/ide/configwin_messages.cmi
> lib/ocaml/coq/ide/coq.cmi
> lib/ocaml/coq/ide/coqOps.cmi
> lib/ocaml/coq/ide/coq_commands.cmi
> @@ -83,19 +99,14 @@ lib/ocaml/coq/ide/document.cmi
> lib/ocaml/coq/ide/fileOps.cmi
> lib/ocaml/coq/ide/gtk_parsing.cmi
> lib/ocaml/coq/ide/ideutils.cmi
> +lib/ocaml/coq/ide/microPG.cmi
> lib/ocaml/coq/ide/minilib.cmi
> -lib/ocaml/coq/ide/nanoPG.cmi
> lib/ocaml/coq/ide/preferences.cmi
> -lib/ocaml/coq/ide/richpp.cmi
> lib/ocaml/coq/ide/sentence.cmi
> -lib/ocaml/coq/ide/serialize.cmi
> lib/ocaml/coq/ide/session.cmi
> lib/ocaml/coq/ide/tags.cmi
> +lib/ocaml/coq/ide/unicode_bindings.cmi
> lib/ocaml/coq/ide/utf8_convert.cmi
> -lib/ocaml/coq/ide/utils/
> -lib/ocaml/coq/ide/utils/configwin.cmi
> -lib/ocaml/coq/ide/utils/configwin_ihm.cmi
> -lib/ocaml/coq/ide/utils/configwin_messages.cmi
> lib/ocaml/coq/ide/wg_Command.cmi
> lib/ocaml/coq/ide/wg_Completion.cmi
> lib/ocaml/coq/ide/wg_Detachable.cmi
> @@ -106,11 +117,8 @@ lib/ocaml/coq/ide/wg_ProofView.cmi
> lib/ocaml/coq/ide/wg_RoutedMessageViews.cmi
> lib/ocaml/coq/ide/wg_ScriptView.cmi
> lib/ocaml/coq/ide/wg_Segment.cmi
> -lib/ocaml/coq/ide/xml_lexer.cmi
> -lib/ocaml/coq/ide/xml_parser.cmi
> -lib/ocaml/coq/ide/xml_printer.cmi
> -lib/ocaml/coq/ide/xmlprotocol.cmi
> lib/ocaml/coq/interp/
> +lib/ocaml/coq/interp/constrexpr.cmi
> lib/ocaml/coq/interp/constrexpr_ops.cmi
> lib/ocaml/coq/interp/constrextern.cmi
> lib/ocaml/coq/interp/constrintern.cmi
> @@ -123,25 +131,12 @@ lib/ocaml/coq/interp/implicit_quantifier
> lib/ocaml/coq/interp/modintern.cmi
> lib/ocaml/coq/interp/notation.cmi
> lib/ocaml/coq/interp/notation_ops.cmi
> -lib/ocaml/coq/interp/ppextend.cmi
> +lib/ocaml/coq/interp/notation_term.cmi
> +lib/ocaml/coq/interp/numTok.cmi
> lib/ocaml/coq/interp/reserve.cmi
> lib/ocaml/coq/interp/smartlocate.cmi
> lib/ocaml/coq/interp/stdarg.cmi
> lib/ocaml/coq/interp/syntax_def.cmi
> -lib/ocaml/coq/interp/tactypes.cmi
> -lib/ocaml/coq/interp/topconstr.cmi
> -lib/ocaml/coq/intf/
> -lib/ocaml/coq/intf/constrexpr.cmi
> -lib/ocaml/coq/intf/decl_kinds.cmi
> -lib/ocaml/coq/intf/evar_kinds.cmi
> -lib/ocaml/coq/intf/extend.cmi
> -lib/ocaml/coq/intf/genredexpr.cmi
> -lib/ocaml/coq/intf/glob_term.cmi
> -lib/ocaml/coq/intf/locus.cmi
> -lib/ocaml/coq/intf/misctypes.cmi
> -lib/ocaml/coq/intf/notation_term.cmi
> -lib/ocaml/coq/intf/pattern.cmi
> -lib/ocaml/coq/intf/vernacexpr.cmi
> lib/ocaml/coq/kernel/
> lib/ocaml/coq/kernel/byterun/
> lib/ocaml/coq/kernel/byterun/dllcoqrun.so
> @@ -151,7 +146,6 @@ lib/ocaml/coq/kernel/cPrimitives.cmi
> lib/ocaml/coq/kernel/cbytecodes.cmi
> lib/ocaml/coq/kernel/cbytegen.cmi
> lib/ocaml/coq/kernel/cemitcodes.cmi
> -lib/ocaml/coq/kernel/cinstr.cmi
> lib/ocaml/coq/kernel/clambda.cmi
> lib/ocaml/coq/kernel/constr.cmi
> lib/ocaml/coq/kernel/context.cmi
> @@ -165,6 +159,7 @@ lib/ocaml/coq/kernel/entries.cmi
> lib/ocaml/coq/kernel/environ.cmi
> lib/ocaml/coq/kernel/esubst.cmi
> lib/ocaml/coq/kernel/evar.cmi
> +lib/ocaml/coq/kernel/indTyping.cmi
> lib/ocaml/coq/kernel/indtypes.cmi
> lib/ocaml/coq/kernel/inductive.cmi
> lib/ocaml/coq/kernel/mod_subst.cmi
> @@ -173,30 +168,32 @@ lib/ocaml/coq/kernel/modops.cmi
> lib/ocaml/coq/kernel/names.cmi
> lib/ocaml/coq/kernel/nativecode.cmi
> lib/ocaml/coq/kernel/nativeconv.cmi
> -lib/ocaml/coq/kernel/nativeinstr.cmi
> lib/ocaml/coq/kernel/nativelambda.cmi
> lib/ocaml/coq/kernel/nativelib.cmi
> lib/ocaml/coq/kernel/nativelibrary.cmi
> lib/ocaml/coq/kernel/nativevalues.cmi
> lib/ocaml/coq/kernel/opaqueproof.cmi
> -lib/ocaml/coq/kernel/pre_env.cmi
> +lib/ocaml/coq/kernel/primred.cmi
> lib/ocaml/coq/kernel/reduction.cmi
> lib/ocaml/coq/kernel/retroknowledge.cmi
> +lib/ocaml/coq/kernel/retypeops.cmi
> lib/ocaml/coq/kernel/safe_typing.cmi
> lib/ocaml/coq/kernel/sorts.cmi
> lib/ocaml/coq/kernel/subtyping.cmi
> lib/ocaml/coq/kernel/term.cmi
> lib/ocaml/coq/kernel/term_typing.cmi
> +lib/ocaml/coq/kernel/transparentState.cmi
> lib/ocaml/coq/kernel/type_errors.cmi
> lib/ocaml/coq/kernel/typeops.cmi
> lib/ocaml/coq/kernel/uGraph.cmi
> -lib/ocaml/coq/kernel/uint31.cmi
> +lib/ocaml/coq/kernel/uint63.cmi
> lib/ocaml/coq/kernel/univ.cmi
> lib/ocaml/coq/kernel/vars.cmi
> lib/ocaml/coq/kernel/vconv.cmi
> lib/ocaml/coq/kernel/vm.cmi
> lib/ocaml/coq/kernel/vmvalues.cmi
> lib/ocaml/coq/lib/
> +lib/ocaml/coq/lib/acyclicGraph.cmi
> lib/ocaml/coq/lib/aux_file.cmi
> lib/ocaml/coq/lib/cAst.cmi
> lib/ocaml/coq/lib/cErrors.cmi
> @@ -214,6 +211,7 @@ lib/ocaml/coq/lib/genarg.cmi
> lib/ocaml/coq/lib/hook.cmi
> lib/ocaml/coq/lib/loc.cmi
> lib/ocaml/coq/lib/pp.cmi
> +lib/ocaml/coq/lib/pp_diff.cmi
> lib/ocaml/coq/lib/remoteCounter.cmi
> lib/ocaml/coq/lib/rtree.cmi
> lib/ocaml/coq/lib/spawn.cmi
> @@ -223,13 +221,12 @@ lib/ocaml/coq/lib/util.cmi
> lib/ocaml/coq/lib/xml_datatype.cmi
> lib/ocaml/coq/library/
> lib/ocaml/coq/library/coqlib.cmi
> +lib/ocaml/coq/library/decl_kinds.cmi
> lib/ocaml/coq/library/declaremods.cmi
> lib/ocaml/coq/library/decls.cmi
> -lib/ocaml/coq/library/dischargedhypsmap.cmi
> lib/ocaml/coq/library/global.cmi
> lib/ocaml/coq/library/globnames.cmi
> lib/ocaml/coq/library/goptions.cmi
> -lib/ocaml/coq/library/heads.cmi
> lib/ocaml/coq/library/keys.cmi
> lib/ocaml/coq/library/kindops.cmi
> lib/ocaml/coq/library/lib.cmi
> @@ -242,13 +239,13 @@ lib/ocaml/coq/library/states.cmi
> lib/ocaml/coq/library/summary.cmi
> lib/ocaml/coq/parsing/
> lib/ocaml/coq/parsing/cLexer.cmi
> -lib/ocaml/coq/parsing/egramcoq.cmi
> -lib/ocaml/coq/parsing/egramml.cmi
> +lib/ocaml/coq/parsing/extend.cmi
> lib/ocaml/coq/parsing/g_constr.cmi
> lib/ocaml/coq/parsing/g_prim.cmi
> -lib/ocaml/coq/parsing/g_proofs.cmi
> -lib/ocaml/coq/parsing/g_vernac.cmi
> +lib/ocaml/coq/parsing/notation_gram.cmi
> +lib/ocaml/coq/parsing/notgram_ops.cmi
> lib/ocaml/coq/parsing/pcoq.cmi
> +lib/ocaml/coq/parsing/ppextend.cmi
> lib/ocaml/coq/parsing/tok.cmi
> lib/ocaml/coq/plugins/
> lib/ocaml/coq/plugins/btauto/
> @@ -266,6 +263,7 @@ lib/ocaml/coq/plugins/btauto/Reflect.glo
> lib/ocaml/coq/plugins/btauto/Reflect.v
> lib/ocaml/coq/plugins/btauto/Reflect.vo
> lib/ocaml/coq/plugins/btauto/btauto_plugin.cmi
> +lib/ocaml/coq/plugins/btauto/refl_btauto.cmi
> lib/ocaml/coq/plugins/cc/
> lib/ocaml/coq/plugins/cc/cc_plugin.cmi
> lib/ocaml/coq/plugins/cc/ccalgo.cmi
> @@ -369,17 +367,6 @@ lib/ocaml/coq/plugins/firstorder/instanc
> lib/ocaml/coq/plugins/firstorder/rules.cmi
> lib/ocaml/coq/plugins/firstorder/sequent.cmi
> lib/ocaml/coq/plugins/firstorder/unify.cmi
> -lib/ocaml/coq/plugins/fourier/
> -lib/ocaml/coq/plugins/fourier/.coq-native/
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmi
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmi
> -lib/ocaml/coq/plugins/fourier/Fourier.glob
> -lib/ocaml/coq/plugins/fourier/Fourier.v
> -lib/ocaml/coq/plugins/fourier/Fourier.vo
> -lib/ocaml/coq/plugins/fourier/Fourier_util.glob
> -lib/ocaml/coq/plugins/fourier/Fourier_util.v
> -lib/ocaml/coq/plugins/fourier/Fourier_util.vo
> -lib/ocaml/coq/plugins/fourier/fourier_plugin.cmi
> lib/ocaml/coq/plugins/funind/
> lib/ocaml/coq/plugins/funind/.coq-native/
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmi
> @@ -428,8 +415,11 @@ lib/ocaml/coq/plugins/ltac/tauto.cmi
> lib/ocaml/coq/plugins/ltac/tauto_plugin.cmi
> lib/ocaml/coq/plugins/micromega/
> lib/ocaml/coq/plugins/micromega/.coq-native/
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmi
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
> @@ -444,12 +434,21 @@ lib/ocaml/coq/plugins/micromega/.coq-nat
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmi
> +lib/ocaml/coq/plugins/micromega/DeclConstant.glob
> +lib/ocaml/coq/plugins/micromega/DeclConstant.v
> +lib/ocaml/coq/plugins/micromega/DeclConstant.vo
> lib/ocaml/coq/plugins/micromega/Env.glob
> lib/ocaml/coq/plugins/micromega/Env.v
> lib/ocaml/coq/plugins/micromega/Env.vo
> lib/ocaml/coq/plugins/micromega/EnvRing.glob
> lib/ocaml/coq/plugins/micromega/EnvRing.v
> lib/ocaml/coq/plugins/micromega/EnvRing.vo
> +lib/ocaml/coq/plugins/micromega/Fourier.glob
> +lib/ocaml/coq/plugins/micromega/Fourier.v
> +lib/ocaml/coq/plugins/micromega/Fourier.vo
> +lib/ocaml/coq/plugins/micromega/Fourier_util.glob
> +lib/ocaml/coq/plugins/micromega/Fourier_util.v
> +lib/ocaml/coq/plugins/micromega/Fourier_util.vo
> lib/ocaml/coq/plugins/micromega/Lia.glob
> lib/ocaml/coq/plugins/micromega/Lia.v
> lib/ocaml/coq/plugins/micromega/Lia.vo
> @@ -492,11 +491,23 @@ lib/ocaml/coq/plugins/micromega/ZCoeff.v
> lib/ocaml/coq/plugins/micromega/ZMicromega.glob
> lib/ocaml/coq/plugins/micromega/ZMicromega.v
> lib/ocaml/coq/plugins/micromega/ZMicromega.vo
> +lib/ocaml/coq/plugins/micromega/certificate.cmi
> +lib/ocaml/coq/plugins/micromega/coq_micromega.cmi
> @bin lib/ocaml/coq/plugins/micromega/csdpcert
> +lib/ocaml/coq/plugins/micromega/csdpcert.cmi
> +lib/ocaml/coq/plugins/micromega/g_micromega.cmi
> +lib/ocaml/coq/plugins/micromega/itv.cmi
> +lib/ocaml/coq/plugins/micromega/mfourier.cmi
> lib/ocaml/coq/plugins/micromega/micromega.cmi
> lib/ocaml/coq/plugins/micromega/micromega_plugin.cmi
> +lib/ocaml/coq/plugins/micromega/mutils.cmi
> +lib/ocaml/coq/plugins/micromega/persistent_cache.cmi
> +lib/ocaml/coq/plugins/micromega/polynomial.cmi
> +lib/ocaml/coq/plugins/micromega/simplex.cmi
> lib/ocaml/coq/plugins/micromega/sos.cmi
> +lib/ocaml/coq/plugins/micromega/sos_lib.cmi
> lib/ocaml/coq/plugins/micromega/sos_types.cmi
> +lib/ocaml/coq/plugins/micromega/vect.cmi
> lib/ocaml/coq/plugins/nsatz/
> lib/ocaml/coq/plugins/nsatz/.coq-native/
> lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
> @@ -530,26 +541,8 @@ lib/ocaml/coq/plugins/omega/OmegaTactic.
> lib/ocaml/coq/plugins/omega/PreOmega.glob
> lib/ocaml/coq/plugins/omega/PreOmega.v
> lib/ocaml/coq/plugins/omega/PreOmega.vo
> +lib/ocaml/coq/plugins/omega/coq_omega.cmi
> lib/ocaml/coq/plugins/omega/omega_plugin.cmi
> -lib/ocaml/coq/plugins/quote/
> -lib/ocaml/coq/plugins/quote/.coq-native/
> -lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
> -lib/ocaml/coq/plugins/quote/Quote.glob
> -lib/ocaml/coq/plugins/quote/Quote.v
> -lib/ocaml/coq/plugins/quote/Quote.vo
> -lib/ocaml/coq/plugins/quote/quote_plugin.cmi
> -lib/ocaml/coq/plugins/romega/
> -lib/ocaml/coq/plugins/romega/.coq-native/
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmi
> -lib/ocaml/coq/plugins/romega/ROmega.glob
> -lib/ocaml/coq/plugins/romega/ROmega.v
> -lib/ocaml/coq/plugins/romega/ROmega.vo
> -lib/ocaml/coq/plugins/romega/ReflOmegaCore.glob
> -lib/ocaml/coq/plugins/romega/ReflOmegaCore.v
> -lib/ocaml/coq/plugins/romega/ReflOmegaCore.vo
> -lib/ocaml/coq/plugins/romega/const_omega.cmi
> -lib/ocaml/coq/plugins/romega/romega_plugin.cmi
> lib/ocaml/coq/plugins/rtauto/
> lib/ocaml/coq/plugins/rtauto/.coq-native/
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
> @@ -694,18 +687,20 @@ lib/ocaml/coq/plugins/ssr/ssrview.cmi
> lib/ocaml/coq/plugins/ssrmatching/
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/
>
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
> +lib/ocaml/coq/plugins/ssrmatching/g_ssrmatching.cmi
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.cmi
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.glob
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.v
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.vo
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
> lib/ocaml/coq/plugins/syntax/
> -lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/numeral.cmi
> +lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/r_syntax.cmi
> lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/string_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/z_syntax_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/string_notation.cmi
> +lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmi
> lib/ocaml/coq/pretyping/
> lib/ocaml/coq/pretyping/arguments_renaming.cmi
> lib/ocaml/coq/pretyping/cases.cmi
> @@ -719,20 +714,23 @@ lib/ocaml/coq/pretyping/evardefine.cmi
> lib/ocaml/coq/pretyping/evarsolve.cmi
> lib/ocaml/coq/pretyping/find_subterm.cmi
> lib/ocaml/coq/pretyping/geninterp.cmi
> +lib/ocaml/coq/pretyping/globEnv.cmi
> lib/ocaml/coq/pretyping/glob_ops.cmi
> +lib/ocaml/coq/pretyping/glob_term.cmi
> +lib/ocaml/coq/pretyping/heads.cmi
> lib/ocaml/coq/pretyping/indrec.cmi
> lib/ocaml/coq/pretyping/inductiveops.cmi
> lib/ocaml/coq/pretyping/inferCumulativity.cmi
> +lib/ocaml/coq/pretyping/locus.cmi
> lib/ocaml/coq/pretyping/locusops.cmi
> lib/ocaml/coq/pretyping/ltac_pretype.cmi
> -lib/ocaml/coq/pretyping/miscops.cmi
> lib/ocaml/coq/pretyping/nativenorm.cmi
> +lib/ocaml/coq/pretyping/pattern.cmi
> lib/ocaml/coq/pretyping/patternops.cmi
> lib/ocaml/coq/pretyping/pretype_errors.cmi
> lib/ocaml/coq/pretyping/pretyping.cmi
> lib/ocaml/coq/pretyping/program.cmi
> lib/ocaml/coq/pretyping/recordops.cmi
> -lib/ocaml/coq/pretyping/redops.cmi
> lib/ocaml/coq/pretyping/reductionops.cmi
> lib/ocaml/coq/pretyping/retyping.cmi
> lib/ocaml/coq/pretyping/tacred.cmi
> @@ -740,32 +738,32 @@ lib/ocaml/coq/pretyping/typeclasses.cmi
> lib/ocaml/coq/pretyping/typeclasses_errors.cmi
> lib/ocaml/coq/pretyping/typing.cmi
> lib/ocaml/coq/pretyping/unification.cmi
> -lib/ocaml/coq/pretyping/univdecls.cmi
> lib/ocaml/coq/pretyping/vnorm.cmi
> lib/ocaml/coq/printing/
> lib/ocaml/coq/printing/genprint.cmi
> lib/ocaml/coq/printing/ppconstr.cmi
> lib/ocaml/coq/printing/pputils.cmi
> -lib/ocaml/coq/printing/ppvernac.cmi
> lib/ocaml/coq/printing/prettyp.cmi
> lib/ocaml/coq/printing/printer.cmi
> lib/ocaml/coq/printing/printmod.cmi
> +lib/ocaml/coq/printing/proof_diffs.cmi
> lib/ocaml/coq/proofs/
> lib/ocaml/coq/proofs/clenv.cmi
> lib/ocaml/coq/proofs/clenvtac.cmi
> lib/ocaml/coq/proofs/evar_refiner.cmi
> lib/ocaml/coq/proofs/goal.cmi
> +lib/ocaml/coq/proofs/goal_select.cmi
> lib/ocaml/coq/proofs/logic.cmi
> lib/ocaml/coq/proofs/miscprint.cmi
> lib/ocaml/coq/proofs/pfedit.cmi
> lib/ocaml/coq/proofs/proof.cmi
> lib/ocaml/coq/proofs/proof_bullet.cmi
> lib/ocaml/coq/proofs/proof_global.cmi
> -lib/ocaml/coq/proofs/proof_type.cmi
> -lib/ocaml/coq/proofs/redexpr.cmi
> lib/ocaml/coq/proofs/refine.cmi
> lib/ocaml/coq/proofs/refiner.cmi
> lib/ocaml/coq/proofs/tacmach.cmi
> +lib/ocaml/coq/proofs/tactypes.cmi
> +lib/ocaml/coq/revision
> lib/ocaml/coq/stm/
> lib/ocaml/coq/stm/asyncTaskQueue.cmi
> lib/ocaml/coq/stm/coqworkmgrApi.cmi
> @@ -777,9 +775,9 @@ lib/ocaml/coq/stm/tQueue.cmi
> lib/ocaml/coq/stm/vcs.cmi
> lib/ocaml/coq/stm/vernac_classifier.cmi
> lib/ocaml/coq/stm/vio_checking.cmi
> -lib/ocaml/coq/stm/workerLoop.cmi
> lib/ocaml/coq/stm/workerPool.cmi
> lib/ocaml/coq/tactics/
> +lib/ocaml/coq/tactics/abstract.cmi
> lib/ocaml/coq/tactics/auto.cmi
> lib/ocaml/coq/tactics/autorewrite.cmi
> lib/ocaml/coq/tactics/btermdn.cmi
> @@ -793,11 +791,15 @@ lib/ocaml/coq/tactics/elimschemes.cmi
> lib/ocaml/coq/tactics/eqdecide.cmi
> lib/ocaml/coq/tactics/eqschemes.cmi
> lib/ocaml/coq/tactics/equality.cmi
> +lib/ocaml/coq/tactics/genredexpr.cmi
> lib/ocaml/coq/tactics/hints.cmi
> lib/ocaml/coq/tactics/hipattern.cmi
> lib/ocaml/coq/tactics/ind_tables.cmi
> lib/ocaml/coq/tactics/inv.cmi
> lib/ocaml/coq/tactics/leminv.cmi
> +lib/ocaml/coq/tactics/ppred.cmi
> +lib/ocaml/coq/tactics/redexpr.cmi
> +lib/ocaml/coq/tactics/redops.cmi
> lib/ocaml/coq/tactics/tacticals.cmi
> lib/ocaml/coq/tactics/tactics.cmi
> lib/ocaml/coq/tactics/term_dnet.cmi
> @@ -987,21 +989,21 @@ lib/ocaml/coq/theories/Classes/SetoidTac
> lib/ocaml/coq/theories/Compat/
> lib/ocaml/coq/theories/Compat/.coq-native/
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmi
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmi
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmi
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmi
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmi
> lib/ocaml/coq/theories/Compat/AdmitAxiom.glob
> lib/ocaml/coq/theories/Compat/AdmitAxiom.v
> lib/ocaml/coq/theories/Compat/AdmitAxiom.vo
> -lib/ocaml/coq/theories/Compat/Coq86.glob
> -lib/ocaml/coq/theories/Compat/Coq86.v
> -lib/ocaml/coq/theories/Compat/Coq86.vo
> -lib/ocaml/coq/theories/Compat/Coq87.glob
> -lib/ocaml/coq/theories/Compat/Coq87.v
> -lib/ocaml/coq/theories/Compat/Coq87.vo
> +lib/ocaml/coq/theories/Compat/Coq810.glob
> +lib/ocaml/coq/theories/Compat/Coq810.v
> +lib/ocaml/coq/theories/Compat/Coq810.vo
> lib/ocaml/coq/theories/Compat/Coq88.glob
> lib/ocaml/coq/theories/Compat/Coq88.v
> lib/ocaml/coq/theories/Compat/Coq88.vo
> +lib/ocaml/coq/theories/Compat/Coq89.glob
> +lib/ocaml/coq/theories/Compat/Coq89.v
> +lib/ocaml/coq/theories/Compat/Coq89.vo
> lib/ocaml/coq/theories/FSets/
> lib/ocaml/coq/theories/FSets/.coq-native/
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
> @@ -1090,6 +1092,7 @@ lib/ocaml/coq/theories/FSets/FSets.v
> lib/ocaml/coq/theories/FSets/FSets.vo
> lib/ocaml/coq/theories/Init/
> lib/ocaml/coq/theories/Init/.coq-native/
> +lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmi
> @@ -1102,6 +1105,9 @@ lib/ocaml/coq/theories/Init/.coq-native/
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmi
> +lib/ocaml/coq/theories/Init/Byte.glob
> +lib/ocaml/coq/theories/Init/Byte.v
> +lib/ocaml/coq/theories/Init/Byte.vo
> lib/ocaml/coq/theories/Init/Datatypes.glob
> lib/ocaml/coq/theories/Init/Datatypes.v
> lib/ocaml/coq/theories/Init/Datatypes.vo
> @@ -1207,6 +1213,7 @@ lib/ocaml/coq/theories/Logic/.coq-native
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmi
> +lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmi
> lib/ocaml/coq/theories/Logic/Berardi.glob
> @@ -1308,6 +1315,9 @@ lib/ocaml/coq/theories/Logic/SetIsType.v
> lib/ocaml/coq/theories/Logic/SetoidChoice.glob
> lib/ocaml/coq/theories/Logic/SetoidChoice.v
> lib/ocaml/coq/theories/Logic/SetoidChoice.vo
> +lib/ocaml/coq/theories/Logic/StrictProp.glob
> +lib/ocaml/coq/theories/Logic/StrictProp.v
> +lib/ocaml/coq/theories/Logic/StrictProp.vo
> lib/ocaml/coq/theories/Logic/WKL.glob
> lib/ocaml/coq/theories/Logic/WKL.v
> lib/ocaml/coq/theories/Logic/WKL.vo
> @@ -1412,6 +1422,7 @@ lib/ocaml/coq/theories/NArith/Nsqrt_def.
> lib/ocaml/coq/theories/NArith/Nsqrt_def.vo
> lib/ocaml/coq/theories/Numbers/
> lib/ocaml/coq/theories/Numbers/.coq-native/
> +lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmi
> @@ -1421,6 +1432,9 @@ lib/ocaml/coq/theories/Numbers/.coq-nati
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmi
> +lib/ocaml/coq/theories/Numbers/AltBinNotations.glob
> +lib/ocaml/coq/theories/Numbers/AltBinNotations.v
> +lib/ocaml/coq/theories/Numbers/AltBinNotations.vo
> lib/ocaml/coq/theories/Numbers/BinNums.glob
> lib/ocaml/coq/theories/Numbers/BinNums.v
> lib/ocaml/coq/theories/Numbers/BinNums.vo
> @@ -1453,6 +1467,20 @@ lib/ocaml/coq/theories/Numbers/Cyclic/In
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Ring31.glob
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Ring31.v
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Ring31.vo
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmi
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmi
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmi
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Cyclic63.glob
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Cyclic63.v
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Cyclic63.vo
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Int63.glob
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Int63.v
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Int63.vo
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Ring63.glob
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Ring63.v
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Ring63.vo
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/
>
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmi
> @@ -1904,6 +1932,7 @@ lib/ocaml/coq/theories/Reals/.coq-native
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmi
> +lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmi
> @@ -2080,6 +2109,9 @@ lib/ocaml/coq/theories/Reals/Rtrigo_fun.
> lib/ocaml/coq/theories/Reals/Rtrigo_reg.glob
> lib/ocaml/coq/theories/Reals/Rtrigo_reg.v
> lib/ocaml/coq/theories/Reals/Rtrigo_reg.vo
> +lib/ocaml/coq/theories/Reals/Runcountable.glob
> +lib/ocaml/coq/theories/Reals/Runcountable.v
> +lib/ocaml/coq/theories/Reals/Runcountable.vo
> lib/ocaml/coq/theories/Reals/SeqProp.glob
> lib/ocaml/coq/theories/Reals/SeqProp.v
> lib/ocaml/coq/theories/Reals/SeqProp.vo
> @@ -2242,10 +2274,30 @@ lib/ocaml/coq/theories/Sorting/Sorting.v
> lib/ocaml/coq/theories/Strings/
> lib/ocaml/coq/theories/Strings/.coq-native/
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmi
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmi
> lib/ocaml/coq/theories/Strings/Ascii.glob
> lib/ocaml/coq/theories/Strings/Ascii.v
> lib/ocaml/coq/theories/Strings/Ascii.vo
> +lib/ocaml/coq/theories/Strings/BinaryString.glob
> +lib/ocaml/coq/theories/Strings/BinaryString.v
> +lib/ocaml/coq/theories/Strings/BinaryString.vo
> +lib/ocaml/coq/theories/Strings/Byte.glob
> +lib/ocaml/coq/theories/Strings/Byte.v
> +lib/ocaml/coq/theories/Strings/Byte.vo
> +lib/ocaml/coq/theories/Strings/ByteVector.glob
> +lib/ocaml/coq/theories/Strings/ByteVector.v
> +lib/ocaml/coq/theories/Strings/ByteVector.vo
> +lib/ocaml/coq/theories/Strings/HexString.glob
> +lib/ocaml/coq/theories/Strings/HexString.v
> +lib/ocaml/coq/theories/Strings/HexString.vo
> +lib/ocaml/coq/theories/Strings/OctalString.glob
> +lib/ocaml/coq/theories/Strings/OctalString.v
> +lib/ocaml/coq/theories/Strings/OctalString.vo
> lib/ocaml/coq/theories/Strings/String.glob
> lib/ocaml/coq/theories/Strings/String.v
> lib/ocaml/coq/theories/Strings/String.vo
> @@ -2520,17 +2572,23 @@ lib/ocaml/coq/tools/coqdoc/coqdoc.sty
> lib/ocaml/coq/tools/make-both-single-timing-files.py
> lib/ocaml/coq/tools/make-both-time-files.py
> lib/ocaml/coq/tools/make-one-time-file.py
> +lib/ocaml/coq/topbin/
> lib/ocaml/coq/toplevel/
> +lib/ocaml/coq/toplevel/ccompile.cmi
> lib/ocaml/coq/toplevel/coqargs.cmi
> +lib/ocaml/coq/toplevel/coqc.cmi
> +lib/ocaml/coq/toplevel/coqcargs.cmi
> lib/ocaml/coq/toplevel/coqinit.cmi
> lib/ocaml/coq/toplevel/coqloop.cmi
> lib/ocaml/coq/toplevel/coqtop.cmi
> +lib/ocaml/coq/toplevel/g_toplevel.cmi
> lib/ocaml/coq/toplevel/usage.cmi
> lib/ocaml/coq/toplevel/vernac.cmi
> -lib/ocaml/coq/toploop/
> +lib/ocaml/coq/toplevel/workerLoop.cmi
> lib/ocaml/coq/user-contrib/
> lib/ocaml/coq/vernac/
> lib/ocaml/coq/vernac/assumptions.cmi
> +lib/ocaml/coq/vernac/attributes.cmi
> lib/ocaml/coq/vernac/auto_ind_decl.cmi
> lib/ocaml/coq/vernac/class.cmi
> lib/ocaml/coq/vernac/classes.cmi
> @@ -2540,7 +2598,11 @@ lib/ocaml/coq/vernac/comFixpoint.cmi
> lib/ocaml/coq/vernac/comInductive.cmi
> lib/ocaml/coq/vernac/comProgramFixpoint.cmi
> lib/ocaml/coq/vernac/declareDef.cmi
> +lib/ocaml/coq/vernac/egramcoq.cmi
> +lib/ocaml/coq/vernac/egramml.cmi
> lib/ocaml/coq/vernac/explainErr.cmi
> +lib/ocaml/coq/vernac/g_proofs.cmi
> +lib/ocaml/coq/vernac/g_vernac.cmi
> lib/ocaml/coq/vernac/himsg.cmi
> lib/ocaml/coq/vernac/indschemes.cmi
> lib/ocaml/coq/vernac/lemmas.cmi
> @@ -2548,12 +2610,15 @@ lib/ocaml/coq/vernac/locality.cmi
> lib/ocaml/coq/vernac/metasyntax.cmi
> lib/ocaml/coq/vernac/mltop.cmi
> lib/ocaml/coq/vernac/obligations.cmi
> +lib/ocaml/coq/vernac/ppvernac.cmi
> lib/ocaml/coq/vernac/proof_using.cmi
> +lib/ocaml/coq/vernac/pvernac.cmi
> lib/ocaml/coq/vernac/record.cmi
> lib/ocaml/coq/vernac/search.cmi
> lib/ocaml/coq/vernac/topfmt.cmi
> lib/ocaml/coq/vernac/vernacentries.cmi
> -lib/ocaml/coq/vernac/vernacinterp.cmi
> +lib/ocaml/coq/vernac/vernacexpr.cmi
> +lib/ocaml/coq/vernac/vernacextend.cmi
> lib/ocaml/coq/vernac/vernacprop.cmi
> lib/ocaml/coq/vernac/vernacstate.cmi
> @man man/man1/coq-tex.1
> @@ -2567,26 +2632,18 @@ lib/ocaml/coq/vernac/vernacstate.cmi
> @man man/man1/coqtop.byte.1
> @man man/man1/coqtop.opt.1
> @man man/man1/coqwc.1
> -@man man/man1/gallina.1
> share/coq/
> share/coq/coq-ssreflect.lang
> share/coq/coq.lang
> share/coq/coq.png
> share/coq/coq_style.xml
> +share/coq/default.bindings
> share/doc/coq/
> -share/doc/coq/CHANGES
> share/doc/coq/CONTRIBUTING.md
> share/doc/coq/CREDITS
> share/doc/coq/FAQ-CoqIde
> share/doc/coq/LICENSE
> share/doc/coq/README.md
> -share/emacs/
> -share/emacs/site-lisp/
> -share/emacs/site-lisp/coq-font-lock.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/
> share/texmf/tex/
> share/texmf/tex/latex/
>
>
> --
> http://gmerlin.de
> OpenPGP: http://gmerlin.de/christopher.pub
> CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1
