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
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 <[email protected]
# 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
pgptlq5vmawdk.pgp
Description: OpenPGP digital signature
