[patch] math/coq 8.10.0 -> 8.11.0

classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

[patch] math/coq 8.10.0 -> 8.11.0

Daniel Dickman
Here's an update of coq to 8.11.0. Only compcert depends on coq and
compcert was just updated to support coq 8.11.0.

Besides the usual bug fixes and cleanups, one of the main changes was the
introduction of Ltac2, a new tactic language.

Note, the diff is fairly big due to the new *.vos files in the PLIST which
are for the new experimental compiled interfaces feature.

ok?

Index: Makefile
===================================================================
RCS file: /cvs/ports/math/coq/Makefile,v
retrieving revision 1.48
diff -u -r1.48 Makefile
--- Makefile 16 Oct 2019 06:40:03 -0000 1.48
+++ Makefile 17 Feb 2020 19:11:02 -0000
@@ -2,7 +2,7 @@
 
 COMMENT= proof assistant based on a typed lambda calculus
 
-V= 8.10.0
+V= 8.11.0
 GH_ACCOUNT = coq
 GH_PROJECT = coq
 GH_TAGNAME = V${V}
Index: distinfo
===================================================================
RCS file: /cvs/ports/math/coq/distinfo,v
retrieving revision 1.17
diff -u -r1.17 distinfo
--- distinfo 16 Oct 2019 06:40:03 -0000 1.17
+++ distinfo 17 Feb 2020 19:11:02 -0000
@@ -1,2 +1,2 @@
-SHA256 (coq-8.10.0.tar.gz) = KSxkFiYgxMSCXDI8HHF2LXZOvJzjm9ju6QCFHqymVfU=
-SIZE (coq-8.10.0.tar.gz) = 6220333
+SHA256 (coq-8.11.0.tar.gz) = 7qEB7/UhfbptEajrEwM+1irLTuimTVyxX9FC5/xdwkg=
+SIZE (coq-8.11.0.tar.gz) = 6555390
Index: patches/patch-Makefile_ide
===================================================================
RCS file: /cvs/ports/math/coq/patches/patch-Makefile_ide,v
retrieving revision 1.2
diff -u -r1.2 patch-Makefile_ide
--- patches/patch-Makefile_ide 6 Sep 2019 22:10:18 -0000 1.2
+++ patches/patch-Makefile_ide 17 Feb 2020 19:11:02 -0000
@@ -3,7 +3,7 @@
 Index: Makefile.ide
 --- Makefile.ide.orig
 +++ Makefile.ide
-@@ -190,7 +190,7 @@ endif
+@@ -187,7 +187,7 @@ endif
  ifeq ($(HASCOQIDE),no)
  install-coqide-byte: install-ide-toploop-byte
  else
Index: patches/patch-configure_ml
===================================================================
RCS file: /cvs/ports/math/coq/patches/patch-configure_ml,v
retrieving revision 1.2
diff -u -r1.2 patch-configure_ml
--- patches/patch-configure_ml 6 Sep 2019 22:10:18 -0000 1.2
+++ patches/patch-configure_ml 17 Feb 2020 19:11:02 -0000
@@ -5,7 +5,7 @@
 Index: configure.ml
 --- configure.ml.orig
 +++ configure.ml
-@@ -940,7 +940,7 @@ let config_runtime () =
+@@ -978,7 +978,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.6
diff -u -r1.6 PFRAG.dynlink-native
--- pkg/PFRAG.dynlink-native 20 Sep 2019 03:28:33 -0000 1.6
+++ pkg/PFRAG.dynlink-native 17 Feb 2020 19:11:03 -0000
@@ -14,6 +14,7 @@
 @bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmxs
 @bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmxs
 @bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
+@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmxs
 @bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
 @bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
 @bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmxs
@@ -51,7 +52,15 @@
 @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmxs
 @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmxs
 @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmxs
+@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Zify.cmxs
+@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmxs
+@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmxs
+@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmxs
+@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmxs
+@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmxs
+@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.cmxs
 @bin lib/ocaml/coq/plugins/micromega/micromega_plugin.cmxs
+@bin lib/ocaml/coq/plugins/micromega/zify_plugin.cmxs
 @bin lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmxs
 @bin lib/ocaml/coq/plugins/nsatz/nsatz_plugin.cmxs
 @bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmxs
@@ -89,11 +98,15 @@
 @bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmxs
 @bin lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmxs
 @bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmxs
+@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.cmxs
 @bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmxs
 @bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmxs
+@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmxs
+@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmxs
 @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/float_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
@@ -144,7 +157,7 @@
 @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_Coq810.cmxs
-@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmxs
+@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.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
@@ -167,6 +180,13 @@
 @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/Floats/.coq-native/NCoq_Floats_FloatAxioms.cmxs
+@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.cmxs
+@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.cmxs
+@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.cmxs
+@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.cmxs
+@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.cmxs
+@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.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
@@ -210,6 +230,7 @@
 @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmxs
 @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FinFun.cmxs
 @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.cmxs
+@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.cmxs
 @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.cmxs
 @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_IndefiniteDescription.cmxs
 @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_JMeq.cmxs
@@ -357,6 +378,13 @@
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ArithProp.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_rel.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_DiscrR.cmxs
@@ -398,6 +426,7 @@
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpow_def.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpower.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsigma.cmxs
 @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsqrt_def.cmxs
@@ -503,7 +532,6 @@
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.cmxs
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmxs
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmxs
-@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.cmxs
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmxs
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmxs
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmxs
@@ -516,6 +544,6 @@
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmxs
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmxs
 @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmxs
-@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/user-contrib/Ltac2/ltac2_plugin.cmxs
Index: pkg/PFRAG.native
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PFRAG.native,v
retrieving revision 1.6
diff -u -r1.6 PFRAG.native
--- pkg/PFRAG.native 7 Oct 2019 06:40:15 -0000 1.6
+++ pkg/PFRAG.native 17 Feb 2020 19:11:06 -0000
@@ -65,6 +65,7 @@
 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.cmx
 lib/ocaml/coq/gramlib/.pack/gramlib.cmxa
 lib/ocaml/coq/gramlib/.pack/gramlib__Gramext.cmx
 lib/ocaml/coq/gramlib/.pack/gramlib__Grammar.cmx
@@ -76,8 +77,8 @@
 lib/ocaml/coq/interp/constrexpr_ops.cmx
 lib/ocaml/coq/interp/constrextern.cmx
 lib/ocaml/coq/interp/constrintern.cmx
-lib/ocaml/coq/interp/declare.cmx
-lib/ocaml/coq/interp/discharge.cmx
+lib/ocaml/coq/interp/decls.cmx
+lib/ocaml/coq/interp/deprecation.cmx
 lib/ocaml/coq/interp/dumpglob.cmx
 lib/ocaml/coq/interp/genintern.cmx
 lib/ocaml/coq/interp/impargs.cmx
@@ -111,9 +112,11 @@
 lib/ocaml/coq/kernel/environ.cmx
 lib/ocaml/coq/kernel/esubst.cmx
 lib/ocaml/coq/kernel/evar.cmx
+lib/ocaml/coq/kernel/float64.cmx
 lib/ocaml/coq/kernel/indTyping.cmx
 lib/ocaml/coq/kernel/indtypes.cmx
 lib/ocaml/coq/kernel/inductive.cmx
+lib/ocaml/coq/kernel/inferCumulativity.cmx
 lib/ocaml/coq/kernel/kernel.a
 lib/ocaml/coq/kernel/kernel.cmxa
 lib/ocaml/coq/kernel/mod_subst.cmx
@@ -132,6 +135,7 @@
 lib/ocaml/coq/kernel/retroknowledge.cmx
 lib/ocaml/coq/kernel/retypeops.cmx
 lib/ocaml/coq/kernel/safe_typing.cmx
+lib/ocaml/coq/kernel/section.cmx
 lib/ocaml/coq/kernel/sorts.cmx
 lib/ocaml/coq/kernel/subtyping.cmx
 lib/ocaml/coq/kernel/term.cmx
@@ -174,21 +178,14 @@
 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/global.cmx
 lib/ocaml/coq/library/globnames.cmx
 lib/ocaml/coq/library/goptions.cmx
-lib/ocaml/coq/library/keys.cmx
-lib/ocaml/coq/library/kindops.cmx
 lib/ocaml/coq/library/lib.cmx
 lib/ocaml/coq/library/libnames.cmx
 lib/ocaml/coq/library/libobject.cmx
-lib/ocaml/coq/library/library.a
-lib/ocaml/coq/library/library.cmx
+@static-lib lib/ocaml/coq/library/library.a
 lib/ocaml/coq/library/library.cmxa
-lib/ocaml/coq/library/loadpath.cmx
 lib/ocaml/coq/library/nametab.cmx
 lib/ocaml/coq/library/states.cmx
 lib/ocaml/coq/library/summary.cmx
@@ -241,6 +238,7 @@
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.o
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o
+lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmx
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmx
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.o
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx
@@ -291,6 +289,7 @@
 lib/ocaml/coq/plugins/funind/functional_principles_proofs.cmx
 lib/ocaml/coq/plugins/funind/functional_principles_types.cmx
 lib/ocaml/coq/plugins/funind/g_indfun.cmx
+lib/ocaml/coq/plugins/funind/gen_principle.cmx
 lib/ocaml/coq/plugins/funind/glob_term_to_relation.cmx
 lib/ocaml/coq/plugins/funind/glob_termops.cmx
 lib/ocaml/coq/plugins/funind/indfun.cmx
@@ -371,10 +370,18 @@
 lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.o
 lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmx
 lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Zify.cmx
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmx
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmx
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmx
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmx
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmx
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.cmx
 lib/ocaml/coq/plugins/micromega/certificate.cmx
 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/g_zify.cmx
 lib/ocaml/coq/plugins/micromega/itv.cmx
 lib/ocaml/coq/plugins/micromega/mfourier.cmx
 lib/ocaml/coq/plugins/micromega/micromega.cmx
@@ -388,6 +395,8 @@
 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/micromega/zify.cmx
+lib/ocaml/coq/plugins/micromega/zify_plugin.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
@@ -476,10 +485,13 @@
 lib/ocaml/coq/plugins/setoid_ring/newring_plugin.o
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmx
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.o
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.cmx
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmx
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.o
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmx
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.o
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmx
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmx
 lib/ocaml/coq/plugins/ssr/ssrbwd.cmx
 lib/ocaml/coq/plugins/ssr/ssrcommon.cmx
 lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmx
@@ -499,6 +511,8 @@
 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/float_syntax.cmx
+lib/ocaml/coq/plugins/syntax/float_syntax_plugin.cmx
 lib/ocaml/coq/plugins/syntax/g_numeral.cmx
 lib/ocaml/coq/plugins/syntax/g_string.cmx
 lib/ocaml/coq/plugins/syntax/int63_syntax.cmx
@@ -531,7 +545,7 @@
 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/keys.cmx
 lib/ocaml/coq/pretyping/locus.cmx
 lib/ocaml/coq/pretyping/locusops.cmx
 lib/ocaml/coq/pretyping/ltac_pretype.cmx
@@ -555,7 +569,6 @@
 lib/ocaml/coq/printing/genprint.cmx
 lib/ocaml/coq/printing/ppconstr.cmx
 lib/ocaml/coq/printing/pputils.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
@@ -568,10 +581,8 @@
 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/proofs.a
 lib/ocaml/coq/proofs/proofs.cmxa
 lib/ocaml/coq/proofs/refine.cmx
@@ -598,6 +609,8 @@
 lib/ocaml/coq/tactics/btermdn.cmx
 lib/ocaml/coq/tactics/class_tactics.cmx
 lib/ocaml/coq/tactics/contradiction.cmx
+lib/ocaml/coq/tactics/declare.cmx
+lib/ocaml/coq/tactics/declareScheme.cmx
 lib/ocaml/coq/tactics/dn.cmx
 lib/ocaml/coq/tactics/dnet.cmx
 lib/ocaml/coq/tactics/eauto.cmx
@@ -612,7 +625,9 @@
 lib/ocaml/coq/tactics/ind_tables.cmx
 lib/ocaml/coq/tactics/inv.cmx
 lib/ocaml/coq/tactics/leminv.cmx
+lib/ocaml/coq/tactics/pfedit.cmx
 lib/ocaml/coq/tactics/ppred.cmx
+lib/ocaml/coq/tactics/proof_global.cmx
 lib/ocaml/coq/tactics/redexpr.cmx
 lib/ocaml/coq/tactics/redops.cmx
 lib/ocaml/coq/tactics/tacticals.cmx
@@ -712,8 +727,7 @@
 lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.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_Coq811.cmx
 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
@@ -758,6 +772,13 @@
 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/Floats/.coq-native/NCoq_Floats_FloatAxioms.cmx
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.cmx
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.cmx
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.cmx
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.cmx
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.cmx
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.cmx
 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
@@ -844,6 +865,7 @@
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FinFun.o
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.cmx
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.o
+lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.cmx
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.cmx
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.o
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_IndefiniteDescription.cmx
@@ -1138,6 +1160,13 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.o
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmx
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmx
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.cmx
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.o
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_rel.cmx
@@ -1220,6 +1249,7 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpower.o
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.cmx
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.cmx
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.cmx
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.o
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsigma.cmx
@@ -1430,8 +1460,6 @@
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.o
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmx
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.o
-lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.cmx
-lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.o
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmx
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.o
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmx
@@ -1456,8 +1484,6 @@
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.o
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmx
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.o
-lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmx
-lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.o
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmx
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
@@ -1481,32 +1507,57 @@
 lib/ocaml/coq/toplevel/usage.cmx
 lib/ocaml/coq/toplevel/vernac.cmx
 lib/ocaml/coq/toplevel/workerLoop.cmx
+lib/ocaml/coq/user-contrib/Ltac2/g_ltac2.cmx
+lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2core.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2dyn.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2entries.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2env.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2extffi.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2ffi.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2intern.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2interp.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2match.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2print.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2quote.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2stdlib.cmx
+lib/ocaml/coq/user-contrib/Ltac2/tac2tactics.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/canonical.cmx
 lib/ocaml/coq/vernac/class.cmx
 lib/ocaml/coq/vernac/classes.cmx
+lib/ocaml/coq/vernac/comArguments.cmx
 lib/ocaml/coq/vernac/comAssumption.cmx
 lib/ocaml/coq/vernac/comDefinition.cmx
 lib/ocaml/coq/vernac/comFixpoint.cmx
 lib/ocaml/coq/vernac/comInductive.cmx
+lib/ocaml/coq/vernac/comPrimitive.cmx
 lib/ocaml/coq/vernac/comProgramFixpoint.cmx
 lib/ocaml/coq/vernac/declareDef.cmx
+lib/ocaml/coq/vernac/declareInd.cmx
+lib/ocaml/coq/vernac/declareObl.cmx
+lib/ocaml/coq/vernac/declareUniv.cmx
+lib/ocaml/coq/vernac/declaremods.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
+lib/ocaml/coq/vernac/library.cmx
+lib/ocaml/coq/vernac/loadpath.cmx
 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/prettyp.cmx
 lib/ocaml/coq/vernac/proof_using.cmx
 lib/ocaml/coq/vernac/pvernac.cmx
+lib/ocaml/coq/vernac/recLemmas.cmx
 lib/ocaml/coq/vernac/record.cmx
 lib/ocaml/coq/vernac/search.cmx
 lib/ocaml/coq/vernac/topfmt.cmx
@@ -1515,5 +1566,37 @@
 lib/ocaml/coq/vernac/vernacentries.cmx
 lib/ocaml/coq/vernac/vernacexpr.cmx
 lib/ocaml/coq/vernac/vernacextend.cmx
+lib/ocaml/coq/vernac/vernacinterp.cmx
 lib/ocaml/coq/vernac/vernacprop.cmx
 lib/ocaml/coq/vernac/vernacstate.cmx
+lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Zify.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.o
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.o
+lib/ocaml/coq/plugins/micromega/zify_plugin.o
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.o
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.o
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.o
+lib/ocaml/coq/plugins/syntax/float_syntax_plugin.o
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.o
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatAxioms.o
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.o
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.o
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.o
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.o
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.o
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.o
+lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.o
+lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.o
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PLIST,v
retrieving revision 1.14
diff -u -r1.14 PLIST
--- pkg/PLIST 7 Oct 2019 06:40:15 -0000 1.14
+++ pkg/PLIST 17 Feb 2020 19:11:07 -0000
@@ -18,6 +18,8 @@
 @comment bin/coqtop.byte
 @bin bin/coqwc
 @bin bin/coqworkmgr
+bin/doc_grammar
+@bin bin/votour
 lib/ocaml/coq/
 lib/ocaml/coq/META
 lib/ocaml/coq/clib/
@@ -61,8 +63,12 @@
 lib/ocaml/coq/coqpp/
 lib/ocaml/coq/coqpp/coqpp_ast.cmi
 lib/ocaml/coq/coqpp/coqpp_parse.cmi
+lib/ocaml/coq/coqpp/coqpp_parser.cmi
 lib/ocaml/coq/dev/
 @comment lib/ocaml/coq/dllcoqrun.so
+lib/ocaml/coq/doc/
+lib/ocaml/coq/doc/tools/
+lib/ocaml/coq/doc/tools/docgram/
 lib/ocaml/coq/engine/
 lib/ocaml/coq/engine/eConstr.cmi
 lib/ocaml/coq/engine/evar_kinds.cmi
@@ -127,8 +133,8 @@
 lib/ocaml/coq/interp/constrexpr_ops.cmi
 lib/ocaml/coq/interp/constrextern.cmi
 lib/ocaml/coq/interp/constrintern.cmi
-lib/ocaml/coq/interp/declare.cmi
-lib/ocaml/coq/interp/discharge.cmi
+lib/ocaml/coq/interp/decls.cmi
+lib/ocaml/coq/interp/deprecation.cmi
 lib/ocaml/coq/interp/dumpglob.cmi
 lib/ocaml/coq/interp/genintern.cmi
 lib/ocaml/coq/interp/impargs.cmi
@@ -144,7 +150,7 @@
 lib/ocaml/coq/interp/syntax_def.cmi
 lib/ocaml/coq/kernel/
 lib/ocaml/coq/kernel/byterun/
-lib/ocaml/coq/kernel/byterun/dllcoqrun.so
+@so lib/ocaml/coq/kernel/byterun/dllcoqrun.so
 @comment lib/ocaml/coq/kernel/byterun/libcoqrun.a
 lib/ocaml/coq/kernel/cClosure.cmi
 lib/ocaml/coq/kernel/cPrimitives.cmi
@@ -164,9 +170,11 @@
 lib/ocaml/coq/kernel/environ.cmi
 lib/ocaml/coq/kernel/esubst.cmi
 lib/ocaml/coq/kernel/evar.cmi
+lib/ocaml/coq/kernel/float64.cmi
 lib/ocaml/coq/kernel/indTyping.cmi
 lib/ocaml/coq/kernel/indtypes.cmi
 lib/ocaml/coq/kernel/inductive.cmi
+lib/ocaml/coq/kernel/inferCumulativity.cmi
 lib/ocaml/coq/kernel/mod_subst.cmi
 lib/ocaml/coq/kernel/mod_typing.cmi
 lib/ocaml/coq/kernel/modops.cmi
@@ -183,6 +191,7 @@
 lib/ocaml/coq/kernel/retroknowledge.cmi
 lib/ocaml/coq/kernel/retypeops.cmi
 lib/ocaml/coq/kernel/safe_typing.cmi
+lib/ocaml/coq/kernel/section.cmi
 lib/ocaml/coq/kernel/sorts.cmi
 lib/ocaml/coq/kernel/subtyping.cmi
 lib/ocaml/coq/kernel/term.cmi
@@ -226,19 +235,12 @@
 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/global.cmi
 lib/ocaml/coq/library/globnames.cmi
 lib/ocaml/coq/library/goptions.cmi
-lib/ocaml/coq/library/keys.cmi
-lib/ocaml/coq/library/kindops.cmi
 lib/ocaml/coq/library/lib.cmi
 lib/ocaml/coq/library/libnames.cmi
 lib/ocaml/coq/library/libobject.cmi
-lib/ocaml/coq/library/library.cmi
-lib/ocaml/coq/library/loadpath.cmi
 lib/ocaml/coq/library/nametab.cmi
 lib/ocaml/coq/library/states.cmi
 lib/ocaml/coq/library/summary.cmi
@@ -261,12 +263,15 @@
 lib/ocaml/coq/plugins/btauto/Algebra.glob
 lib/ocaml/coq/plugins/btauto/Algebra.v
 lib/ocaml/coq/plugins/btauto/Algebra.vo
+lib/ocaml/coq/plugins/btauto/Algebra.vos
 lib/ocaml/coq/plugins/btauto/Btauto.glob
 lib/ocaml/coq/plugins/btauto/Btauto.v
 lib/ocaml/coq/plugins/btauto/Btauto.vo
+lib/ocaml/coq/plugins/btauto/Btauto.vos
 lib/ocaml/coq/plugins/btauto/Reflect.glob
 lib/ocaml/coq/plugins/btauto/Reflect.v
 lib/ocaml/coq/plugins/btauto/Reflect.vo
+lib/ocaml/coq/plugins/btauto/Reflect.vos
 lib/ocaml/coq/plugins/btauto/btauto_plugin.cmi
 lib/ocaml/coq/plugins/btauto/refl_btauto.cmi
 lib/ocaml/coq/plugins/cc/
@@ -280,6 +285,7 @@
 lib/ocaml/coq/plugins/derive/Derive.glob
 lib/ocaml/coq/plugins/derive/Derive.v
 lib/ocaml/coq/plugins/derive/Derive.vo
+lib/ocaml/coq/plugins/derive/Derive.vos
 lib/ocaml/coq/plugins/derive/derive.cmi
 lib/ocaml/coq/plugins/derive/derive_plugin.cmi
 lib/ocaml/coq/plugins/extraction/
@@ -292,6 +298,7 @@
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmi
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmi
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmi
+lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmi
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmi
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
 lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmi
@@ -305,57 +312,79 @@
 lib/ocaml/coq/plugins/extraction/ExtrHaskellBasic.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellBasic.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellBasic.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellBasic.vos
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInt.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInt.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInt.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInt.vos
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInteger.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInteger.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInteger.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellNatInteger.vos
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatNum.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatNum.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellNatNum.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellNatNum.vos
 lib/ocaml/coq/plugins/extraction/ExtrHaskellString.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellString.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellString.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellString.vos
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZInt.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZInt.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZInt.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellZInt.vos
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZInteger.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZInteger.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZInteger.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellZInteger.vos
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZNum.glob
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZNum.v
 lib/ocaml/coq/plugins/extraction/ExtrHaskellZNum.vo
+lib/ocaml/coq/plugins/extraction/ExtrHaskellZNum.vos
+lib/ocaml/coq/plugins/extraction/ExtrOCamlFloats.glob
+lib/ocaml/coq/plugins/extraction/ExtrOCamlFloats.v
+lib/ocaml/coq/plugins/extraction/ExtrOCamlFloats.vo
+lib/ocaml/coq/plugins/extraction/ExtrOCamlFloats.vos
 lib/ocaml/coq/plugins/extraction/ExtrOCamlInt63.glob
 lib/ocaml/coq/plugins/extraction/ExtrOCamlInt63.v
 lib/ocaml/coq/plugins/extraction/ExtrOCamlInt63.vo
+lib/ocaml/coq/plugins/extraction/ExtrOCamlInt63.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlBasic.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlBasic.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlBasic.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlBasic.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlBigIntConv.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlBigIntConv.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlBigIntConv.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlBigIntConv.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlIntConv.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlIntConv.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlIntConv.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlIntConv.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlNatBigInt.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlNatBigInt.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlNatBigInt.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlNatBigInt.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlNatInt.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlNatInt.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlNatInt.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlNatInt.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlString.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlString.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlString.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlString.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlZBigInt.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlZBigInt.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlZBigInt.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlZBigInt.vos
 lib/ocaml/coq/plugins/extraction/ExtrOcamlZInt.glob
 lib/ocaml/coq/plugins/extraction/ExtrOcamlZInt.v
 lib/ocaml/coq/plugins/extraction/ExtrOcamlZInt.vo
+lib/ocaml/coq/plugins/extraction/ExtrOcamlZInt.vos
 lib/ocaml/coq/plugins/extraction/Extraction.glob
 lib/ocaml/coq/plugins/extraction/Extraction.v
 lib/ocaml/coq/plugins/extraction/Extraction.vo
+lib/ocaml/coq/plugins/extraction/Extraction.vos
 lib/ocaml/coq/plugins/extraction/common.cmi
 lib/ocaml/coq/plugins/extraction/extract_env.cmi
 lib/ocaml/coq/plugins/extraction/extraction.cmi
@@ -383,11 +412,14 @@
 lib/ocaml/coq/plugins/funind/FunInd.glob
 lib/ocaml/coq/plugins/funind/FunInd.v
 lib/ocaml/coq/plugins/funind/FunInd.vo
+lib/ocaml/coq/plugins/funind/FunInd.vos
 lib/ocaml/coq/plugins/funind/Recdef.glob
 lib/ocaml/coq/plugins/funind/Recdef.v
 lib/ocaml/coq/plugins/funind/Recdef.vo
+lib/ocaml/coq/plugins/funind/Recdef.vos
 lib/ocaml/coq/plugins/funind/functional_principles_proofs.cmi
 lib/ocaml/coq/plugins/funind/functional_principles_types.cmi
+lib/ocaml/coq/plugins/funind/gen_principle.cmi
 lib/ocaml/coq/plugins/funind/glob_term_to_relation.cmi
 lib/ocaml/coq/plugins/funind/glob_termops.cmi
 lib/ocaml/coq/plugins/funind/indfun.cmi
@@ -401,6 +433,7 @@
 lib/ocaml/coq/plugins/ltac/Ltac.glob
 lib/ocaml/coq/plugins/ltac/Ltac.v
 lib/ocaml/coq/plugins/ltac/Ltac.vo
+lib/ocaml/coq/plugins/ltac/Ltac.vos
 lib/ocaml/coq/plugins/ltac/evar_tactics.cmi
 lib/ocaml/coq/plugins/ltac/extraargs.cmi
 lib/ocaml/coq/plugins/ltac/extratactics.cmi
@@ -443,63 +476,117 @@
 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/.coq-native/NCoq_micromega_Zify.cmi
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmi
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmi
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmi
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmi
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmi
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.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/DeclConstant.vos
 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/Env.vos
 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/EnvRing.vos
 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.vos
 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/Fourier_util.vos
 lib/ocaml/coq/plugins/micromega/Lia.glob
 lib/ocaml/coq/plugins/micromega/Lia.v
 lib/ocaml/coq/plugins/micromega/Lia.vo
+lib/ocaml/coq/plugins/micromega/Lia.vos
 lib/ocaml/coq/plugins/micromega/Lqa.glob
 lib/ocaml/coq/plugins/micromega/Lqa.v
 lib/ocaml/coq/plugins/micromega/Lqa.vo
+lib/ocaml/coq/plugins/micromega/Lqa.vos
 lib/ocaml/coq/plugins/micromega/Lra.glob
 lib/ocaml/coq/plugins/micromega/Lra.v
 lib/ocaml/coq/plugins/micromega/Lra.vo
+lib/ocaml/coq/plugins/micromega/Lra.vos
 lib/ocaml/coq/plugins/micromega/MExtraction.glob
 lib/ocaml/coq/plugins/micromega/MExtraction.v
 lib/ocaml/coq/plugins/micromega/MExtraction.vo
+lib/ocaml/coq/plugins/micromega/MExtraction.vos
 lib/ocaml/coq/plugins/micromega/OrderedRing.glob
 lib/ocaml/coq/plugins/micromega/OrderedRing.v
 lib/ocaml/coq/plugins/micromega/OrderedRing.vo
+lib/ocaml/coq/plugins/micromega/OrderedRing.vos
 lib/ocaml/coq/plugins/micromega/Psatz.glob
 lib/ocaml/coq/plugins/micromega/Psatz.v
 lib/ocaml/coq/plugins/micromega/Psatz.vo
+lib/ocaml/coq/plugins/micromega/Psatz.vos
 lib/ocaml/coq/plugins/micromega/QMicromega.glob
 lib/ocaml/coq/plugins/micromega/QMicromega.v
 lib/ocaml/coq/plugins/micromega/QMicromega.vo
+lib/ocaml/coq/plugins/micromega/QMicromega.vos
 lib/ocaml/coq/plugins/micromega/RMicromega.glob
 lib/ocaml/coq/plugins/micromega/RMicromega.v
 lib/ocaml/coq/plugins/micromega/RMicromega.vo
+lib/ocaml/coq/plugins/micromega/RMicromega.vos
 lib/ocaml/coq/plugins/micromega/Refl.glob
 lib/ocaml/coq/plugins/micromega/Refl.v
 lib/ocaml/coq/plugins/micromega/Refl.vo
+lib/ocaml/coq/plugins/micromega/Refl.vos
 lib/ocaml/coq/plugins/micromega/RingMicromega.glob
 lib/ocaml/coq/plugins/micromega/RingMicromega.v
 lib/ocaml/coq/plugins/micromega/RingMicromega.vo
+lib/ocaml/coq/plugins/micromega/RingMicromega.vos
 lib/ocaml/coq/plugins/micromega/Tauto.glob
 lib/ocaml/coq/plugins/micromega/Tauto.v
 lib/ocaml/coq/plugins/micromega/Tauto.vo
+lib/ocaml/coq/plugins/micromega/Tauto.vos
 lib/ocaml/coq/plugins/micromega/VarMap.glob
 lib/ocaml/coq/plugins/micromega/VarMap.v
 lib/ocaml/coq/plugins/micromega/VarMap.vo
+lib/ocaml/coq/plugins/micromega/VarMap.vos
 lib/ocaml/coq/plugins/micromega/ZCoeff.glob
 lib/ocaml/coq/plugins/micromega/ZCoeff.v
 lib/ocaml/coq/plugins/micromega/ZCoeff.vo
+lib/ocaml/coq/plugins/micromega/ZCoeff.vos
 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/ZMicromega.vos
+lib/ocaml/coq/plugins/micromega/Zify.glob
+lib/ocaml/coq/plugins/micromega/Zify.v
+lib/ocaml/coq/plugins/micromega/Zify.vo
+lib/ocaml/coq/plugins/micromega/Zify.vos
+lib/ocaml/coq/plugins/micromega/ZifyBool.glob
+lib/ocaml/coq/plugins/micromega/ZifyBool.v
+lib/ocaml/coq/plugins/micromega/ZifyBool.vo
+lib/ocaml/coq/plugins/micromega/ZifyBool.vos
+lib/ocaml/coq/plugins/micromega/ZifyClasses.glob
+lib/ocaml/coq/plugins/micromega/ZifyClasses.v
+lib/ocaml/coq/plugins/micromega/ZifyClasses.vo
+lib/ocaml/coq/plugins/micromega/ZifyClasses.vos
+lib/ocaml/coq/plugins/micromega/ZifyComparison.glob
+lib/ocaml/coq/plugins/micromega/ZifyComparison.v
+lib/ocaml/coq/plugins/micromega/ZifyComparison.vo
+lib/ocaml/coq/plugins/micromega/ZifyComparison.vos
+lib/ocaml/coq/plugins/micromega/ZifyInst.glob
+lib/ocaml/coq/plugins/micromega/ZifyInst.v
+lib/ocaml/coq/plugins/micromega/ZifyInst.vo
+lib/ocaml/coq/plugins/micromega/ZifyInst.vos
+lib/ocaml/coq/plugins/micromega/ZifyPow.glob
+lib/ocaml/coq/plugins/micromega/ZifyPow.v
+lib/ocaml/coq/plugins/micromega/ZifyPow.vo
+lib/ocaml/coq/plugins/micromega/ZifyPow.vos
+lib/ocaml/coq/plugins/micromega/Ztac.glob
+lib/ocaml/coq/plugins/micromega/Ztac.v
+lib/ocaml/coq/plugins/micromega/Ztac.vo
+lib/ocaml/coq/plugins/micromega/Ztac.vos
 lib/ocaml/coq/plugins/micromega/certificate.cmi
 lib/ocaml/coq/plugins/micromega/coq_micromega.cmi
 @bin lib/ocaml/coq/plugins/micromega/csdpcert
@@ -517,12 +604,15 @@
 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/micromega/zify.cmi
+lib/ocaml/coq/plugins/micromega/zify_plugin.cmi
 lib/ocaml/coq/plugins/nsatz/
 lib/ocaml/coq/plugins/nsatz/.coq-native/
 lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
 lib/ocaml/coq/plugins/nsatz/Nsatz.glob
 lib/ocaml/coq/plugins/nsatz/Nsatz.v
 lib/ocaml/coq/plugins/nsatz/Nsatz.vo
+lib/ocaml/coq/plugins/nsatz/Nsatz.vos
 lib/ocaml/coq/plugins/nsatz/ideal.cmi
 lib/ocaml/coq/plugins/nsatz/nsatz.cmi
 lib/ocaml/coq/plugins/nsatz/nsatz_plugin.cmi
@@ -538,18 +628,23 @@
 lib/ocaml/coq/plugins/omega/Omega.glob
 lib/ocaml/coq/plugins/omega/Omega.v
 lib/ocaml/coq/plugins/omega/Omega.vo
+lib/ocaml/coq/plugins/omega/Omega.vos
 lib/ocaml/coq/plugins/omega/OmegaLemmas.glob
 lib/ocaml/coq/plugins/omega/OmegaLemmas.v
 lib/ocaml/coq/plugins/omega/OmegaLemmas.vo
+lib/ocaml/coq/plugins/omega/OmegaLemmas.vos
 lib/ocaml/coq/plugins/omega/OmegaPlugin.glob
 lib/ocaml/coq/plugins/omega/OmegaPlugin.v
 lib/ocaml/coq/plugins/omega/OmegaPlugin.vo
+lib/ocaml/coq/plugins/omega/OmegaPlugin.vos
 lib/ocaml/coq/plugins/omega/OmegaTactic.glob
 lib/ocaml/coq/plugins/omega/OmegaTactic.v
 lib/ocaml/coq/plugins/omega/OmegaTactic.vo
+lib/ocaml/coq/plugins/omega/OmegaTactic.vos
 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/PreOmega.vos
 lib/ocaml/coq/plugins/omega/coq_omega.cmi
 lib/ocaml/coq/plugins/omega/omega_plugin.cmi
 lib/ocaml/coq/plugins/rtauto/
@@ -559,9 +654,11 @@
 lib/ocaml/coq/plugins/rtauto/Bintree.glob
 lib/ocaml/coq/plugins/rtauto/Bintree.v
 lib/ocaml/coq/plugins/rtauto/Bintree.vo
+lib/ocaml/coq/plugins/rtauto/Bintree.vos
 lib/ocaml/coq/plugins/rtauto/Rtauto.glob
 lib/ocaml/coq/plugins/rtauto/Rtauto.v
 lib/ocaml/coq/plugins/rtauto/Rtauto.vo
+lib/ocaml/coq/plugins/rtauto/Rtauto.vos
 lib/ocaml/coq/plugins/rtauto/proof_search.cmi
 lib/ocaml/coq/plugins/rtauto/refl_tauto.cmi
 lib/ocaml/coq/plugins/rtauto/rtauto_plugin.cmi
@@ -594,103 +691,145 @@
 lib/ocaml/coq/plugins/setoid_ring/Algebra_syntax.glob
 lib/ocaml/coq/plugins/setoid_ring/Algebra_syntax.v
 lib/ocaml/coq/plugins/setoid_ring/Algebra_syntax.vo
+lib/ocaml/coq/plugins/setoid_ring/Algebra_syntax.vos
 lib/ocaml/coq/plugins/setoid_ring/ArithRing.glob
 lib/ocaml/coq/plugins/setoid_ring/ArithRing.v
 lib/ocaml/coq/plugins/setoid_ring/ArithRing.vo
+lib/ocaml/coq/plugins/setoid_ring/ArithRing.vos
 lib/ocaml/coq/plugins/setoid_ring/BinList.glob
 lib/ocaml/coq/plugins/setoid_ring/BinList.v
 lib/ocaml/coq/plugins/setoid_ring/BinList.vo
+lib/ocaml/coq/plugins/setoid_ring/BinList.vos
 lib/ocaml/coq/plugins/setoid_ring/Cring.glob
 lib/ocaml/coq/plugins/setoid_ring/Cring.v
 lib/ocaml/coq/plugins/setoid_ring/Cring.vo
+lib/ocaml/coq/plugins/setoid_ring/Cring.vos
 lib/ocaml/coq/plugins/setoid_ring/Field.glob
 lib/ocaml/coq/plugins/setoid_ring/Field.v
 lib/ocaml/coq/plugins/setoid_ring/Field.vo
+lib/ocaml/coq/plugins/setoid_ring/Field.vos
 lib/ocaml/coq/plugins/setoid_ring/Field_tac.glob
 lib/ocaml/coq/plugins/setoid_ring/Field_tac.v
 lib/ocaml/coq/plugins/setoid_ring/Field_tac.vo
+lib/ocaml/coq/plugins/setoid_ring/Field_tac.vos
 lib/ocaml/coq/plugins/setoid_ring/Field_theory.glob
 lib/ocaml/coq/plugins/setoid_ring/Field_theory.v
 lib/ocaml/coq/plugins/setoid_ring/Field_theory.vo
+lib/ocaml/coq/plugins/setoid_ring/Field_theory.vos
 lib/ocaml/coq/plugins/setoid_ring/InitialRing.glob
 lib/ocaml/coq/plugins/setoid_ring/InitialRing.v
 lib/ocaml/coq/plugins/setoid_ring/InitialRing.vo
+lib/ocaml/coq/plugins/setoid_ring/InitialRing.vos
 lib/ocaml/coq/plugins/setoid_ring/Integral_domain.glob
 lib/ocaml/coq/plugins/setoid_ring/Integral_domain.v
 lib/ocaml/coq/plugins/setoid_ring/Integral_domain.vo
+lib/ocaml/coq/plugins/setoid_ring/Integral_domain.vos
 lib/ocaml/coq/plugins/setoid_ring/NArithRing.glob
 lib/ocaml/coq/plugins/setoid_ring/NArithRing.v
 lib/ocaml/coq/plugins/setoid_ring/NArithRing.vo
+lib/ocaml/coq/plugins/setoid_ring/NArithRing.vos
 lib/ocaml/coq/plugins/setoid_ring/Ncring.glob
 lib/ocaml/coq/plugins/setoid_ring/Ncring.v
 lib/ocaml/coq/plugins/setoid_ring/Ncring.vo
+lib/ocaml/coq/plugins/setoid_ring/Ncring.vos
 lib/ocaml/coq/plugins/setoid_ring/Ncring_initial.glob
 lib/ocaml/coq/plugins/setoid_ring/Ncring_initial.v
 lib/ocaml/coq/plugins/setoid_ring/Ncring_initial.vo
+lib/ocaml/coq/plugins/setoid_ring/Ncring_initial.vos
 lib/ocaml/coq/plugins/setoid_ring/Ncring_polynom.glob
 lib/ocaml/coq/plugins/setoid_ring/Ncring_polynom.v
 lib/ocaml/coq/plugins/setoid_ring/Ncring_polynom.vo
+lib/ocaml/coq/plugins/setoid_ring/Ncring_polynom.vos
 lib/ocaml/coq/plugins/setoid_ring/Ncring_tac.glob
 lib/ocaml/coq/plugins/setoid_ring/Ncring_tac.v
 lib/ocaml/coq/plugins/setoid_ring/Ncring_tac.vo
+lib/ocaml/coq/plugins/setoid_ring/Ncring_tac.vos
 lib/ocaml/coq/plugins/setoid_ring/RealField.glob
 lib/ocaml/coq/plugins/setoid_ring/RealField.v
 lib/ocaml/coq/plugins/setoid_ring/RealField.vo
+lib/ocaml/coq/plugins/setoid_ring/RealField.vos
 lib/ocaml/coq/plugins/setoid_ring/Ring.glob
 lib/ocaml/coq/plugins/setoid_ring/Ring.v
 lib/ocaml/coq/plugins/setoid_ring/Ring.vo
+lib/ocaml/coq/plugins/setoid_ring/Ring.vos
 lib/ocaml/coq/plugins/setoid_ring/Ring_base.glob
 lib/ocaml/coq/plugins/setoid_ring/Ring_base.v
 lib/ocaml/coq/plugins/setoid_ring/Ring_base.vo
+lib/ocaml/coq/plugins/setoid_ring/Ring_base.vos
 lib/ocaml/coq/plugins/setoid_ring/Ring_polynom.glob
 lib/ocaml/coq/plugins/setoid_ring/Ring_polynom.v
 lib/ocaml/coq/plugins/setoid_ring/Ring_polynom.vo
+lib/ocaml/coq/plugins/setoid_ring/Ring_polynom.vos
 lib/ocaml/coq/plugins/setoid_ring/Ring_tac.glob
 lib/ocaml/coq/plugins/setoid_ring/Ring_tac.v
 lib/ocaml/coq/plugins/setoid_ring/Ring_tac.vo
+lib/ocaml/coq/plugins/setoid_ring/Ring_tac.vos
 lib/ocaml/coq/plugins/setoid_ring/Ring_theory.glob
 lib/ocaml/coq/plugins/setoid_ring/Ring_theory.v
 lib/ocaml/coq/plugins/setoid_ring/Ring_theory.vo
+lib/ocaml/coq/plugins/setoid_ring/Ring_theory.vos
 lib/ocaml/coq/plugins/setoid_ring/Rings_Q.glob
 lib/ocaml/coq/plugins/setoid_ring/Rings_Q.v
 lib/ocaml/coq/plugins/setoid_ring/Rings_Q.vo
+lib/ocaml/coq/plugins/setoid_ring/Rings_Q.vos
 lib/ocaml/coq/plugins/setoid_ring/Rings_R.glob
 lib/ocaml/coq/plugins/setoid_ring/Rings_R.v
 lib/ocaml/coq/plugins/setoid_ring/Rings_R.vo
+lib/ocaml/coq/plugins/setoid_ring/Rings_R.vos
 lib/ocaml/coq/plugins/setoid_ring/Rings_Z.glob
 lib/ocaml/coq/plugins/setoid_ring/Rings_Z.v
 lib/ocaml/coq/plugins/setoid_ring/Rings_Z.vo
+lib/ocaml/coq/plugins/setoid_ring/Rings_Z.vos
 lib/ocaml/coq/plugins/setoid_ring/ZArithRing.glob
 lib/ocaml/coq/plugins/setoid_ring/ZArithRing.v
 lib/ocaml/coq/plugins/setoid_ring/ZArithRing.vo
+lib/ocaml/coq/plugins/setoid_ring/ZArithRing.vos
 lib/ocaml/coq/plugins/setoid_ring/newring.cmi
 lib/ocaml/coq/plugins/setoid_ring/newring_ast.cmi
 lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmi
 lib/ocaml/coq/plugins/ssr/
 lib/ocaml/coq/plugins/ssr/.coq-native/
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmi
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.cmi
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmi
 lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmi
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmi
+lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmi
 lib/ocaml/coq/plugins/ssr/ssrast.cmi
 lib/ocaml/coq/plugins/ssr/ssrbool.glob
 lib/ocaml/coq/plugins/ssr/ssrbool.v
 lib/ocaml/coq/plugins/ssr/ssrbool.vo
+lib/ocaml/coq/plugins/ssr/ssrbool.vos
 lib/ocaml/coq/plugins/ssr/ssrbwd.cmi
+lib/ocaml/coq/plugins/ssr/ssrclasses.glob
+lib/ocaml/coq/plugins/ssr/ssrclasses.v
+lib/ocaml/coq/plugins/ssr/ssrclasses.vo
+lib/ocaml/coq/plugins/ssr/ssrclasses.vos
 lib/ocaml/coq/plugins/ssr/ssrcommon.cmi
 lib/ocaml/coq/plugins/ssr/ssreflect.glob
 lib/ocaml/coq/plugins/ssr/ssreflect.v
 lib/ocaml/coq/plugins/ssr/ssreflect.vo
+lib/ocaml/coq/plugins/ssr/ssreflect.vos
 lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmi
 lib/ocaml/coq/plugins/ssr/ssrelim.cmi
 lib/ocaml/coq/plugins/ssr/ssrequality.cmi
 lib/ocaml/coq/plugins/ssr/ssrfun.glob
 lib/ocaml/coq/plugins/ssr/ssrfun.v
 lib/ocaml/coq/plugins/ssr/ssrfun.vo
+lib/ocaml/coq/plugins/ssr/ssrfun.vos
 lib/ocaml/coq/plugins/ssr/ssrfwd.cmi
 lib/ocaml/coq/plugins/ssr/ssripats.cmi
 lib/ocaml/coq/plugins/ssr/ssrparser.cmi
 lib/ocaml/coq/plugins/ssr/ssrprinters.cmi
+lib/ocaml/coq/plugins/ssr/ssrsetoid.glob
+lib/ocaml/coq/plugins/ssr/ssrsetoid.v
+lib/ocaml/coq/plugins/ssr/ssrsetoid.vo
+lib/ocaml/coq/plugins/ssr/ssrsetoid.vos
 lib/ocaml/coq/plugins/ssr/ssrtacticals.cmi
+lib/ocaml/coq/plugins/ssr/ssrunder.glob
+lib/ocaml/coq/plugins/ssr/ssrunder.v
+lib/ocaml/coq/plugins/ssr/ssrunder.vo
+lib/ocaml/coq/plugins/ssr/ssrunder.vos
 lib/ocaml/coq/plugins/ssr/ssrvernac.cmi
 lib/ocaml/coq/plugins/ssr/ssrview.cmi
 lib/ocaml/coq/plugins/ssrmatching/
@@ -701,8 +840,10 @@
 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.vos
 lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
 lib/ocaml/coq/plugins/syntax/
+lib/ocaml/coq/plugins/syntax/float_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
@@ -729,7 +870,7 @@
 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/keys.cmi
 lib/ocaml/coq/pretyping/locus.cmi
 lib/ocaml/coq/pretyping/locusops.cmi
 lib/ocaml/coq/pretyping/ltac_pretype.cmi
@@ -752,7 +893,6 @@
 lib/ocaml/coq/printing/genprint.cmi
 lib/ocaml/coq/printing/ppconstr.cmi
 lib/ocaml/coq/printing/pputils.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
@@ -764,10 +904,8 @@
 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/refine.cmi
 lib/ocaml/coq/proofs/refiner.cmi
 lib/ocaml/coq/proofs/tacmach.cmi
@@ -791,6 +929,8 @@
 lib/ocaml/coq/tactics/btermdn.cmi
 lib/ocaml/coq/tactics/class_tactics.cmi
 lib/ocaml/coq/tactics/contradiction.cmi
+lib/ocaml/coq/tactics/declare.cmi
+lib/ocaml/coq/tactics/declareScheme.cmi
 lib/ocaml/coq/tactics/dn.cmi
 lib/ocaml/coq/tactics/dnet.cmi
 lib/ocaml/coq/tactics/eauto.cmi
@@ -805,7 +945,9 @@
 lib/ocaml/coq/tactics/ind_tables.cmi
 lib/ocaml/coq/tactics/inv.cmi
 lib/ocaml/coq/tactics/leminv.cmi
+lib/ocaml/coq/tactics/pfedit.cmi
 lib/ocaml/coq/tactics/ppred.cmi
+lib/ocaml/coq/tactics/proof_global.cmi
 lib/ocaml/coq/tactics/redexpr.cmi
 lib/ocaml/coq/tactics/redops.cmi
 lib/ocaml/coq/tactics/tacticals.cmi
@@ -839,69 +981,91 @@
 lib/ocaml/coq/theories/Arith/Arith.glob
 lib/ocaml/coq/theories/Arith/Arith.v
 lib/ocaml/coq/theories/Arith/Arith.vo
+lib/ocaml/coq/theories/Arith/Arith.vos
 lib/ocaml/coq/theories/Arith/Arith_base.glob
 lib/ocaml/coq/theories/Arith/Arith_base.v
 lib/ocaml/coq/theories/Arith/Arith_base.vo
+lib/ocaml/coq/theories/Arith/Arith_base.vos
 lib/ocaml/coq/theories/Arith/Between.glob
 lib/ocaml/coq/theories/Arith/Between.v
 lib/ocaml/coq/theories/Arith/Between.vo
+lib/ocaml/coq/theories/Arith/Between.vos
 lib/ocaml/coq/theories/Arith/Bool_nat.glob
 lib/ocaml/coq/theories/Arith/Bool_nat.v
 lib/ocaml/coq/theories/Arith/Bool_nat.vo
+lib/ocaml/coq/theories/Arith/Bool_nat.vos
 lib/ocaml/coq/theories/Arith/Compare.glob
 lib/ocaml/coq/theories/Arith/Compare.v
 lib/ocaml/coq/theories/Arith/Compare.vo
+lib/ocaml/coq/theories/Arith/Compare.vos
 lib/ocaml/coq/theories/Arith/Compare_dec.glob
 lib/ocaml/coq/theories/Arith/Compare_dec.v
 lib/ocaml/coq/theories/Arith/Compare_dec.vo
+lib/ocaml/coq/theories/Arith/Compare_dec.vos
 lib/ocaml/coq/theories/Arith/Div2.glob
 lib/ocaml/coq/theories/Arith/Div2.v
 lib/ocaml/coq/theories/Arith/Div2.vo
+lib/ocaml/coq/theories/Arith/Div2.vos
 lib/ocaml/coq/theories/Arith/EqNat.glob
 lib/ocaml/coq/theories/Arith/EqNat.v
 lib/ocaml/coq/theories/Arith/EqNat.vo
+lib/ocaml/coq/theories/Arith/EqNat.vos
 lib/ocaml/coq/theories/Arith/Euclid.glob
 lib/ocaml/coq/theories/Arith/Euclid.v
 lib/ocaml/coq/theories/Arith/Euclid.vo
+lib/ocaml/coq/theories/Arith/Euclid.vos
 lib/ocaml/coq/theories/Arith/Even.glob
 lib/ocaml/coq/theories/Arith/Even.v
 lib/ocaml/coq/theories/Arith/Even.vo
+lib/ocaml/coq/theories/Arith/Even.vos
 lib/ocaml/coq/theories/Arith/Factorial.glob
 lib/ocaml/coq/theories/Arith/Factorial.v
 lib/ocaml/coq/theories/Arith/Factorial.vo
+lib/ocaml/coq/theories/Arith/Factorial.vos
 lib/ocaml/coq/theories/Arith/Gt.glob
 lib/ocaml/coq/theories/Arith/Gt.v
 lib/ocaml/coq/theories/Arith/Gt.vo
+lib/ocaml/coq/theories/Arith/Gt.vos
 lib/ocaml/coq/theories/Arith/Le.glob
 lib/ocaml/coq/theories/Arith/Le.v
 lib/ocaml/coq/theories/Arith/Le.vo
+lib/ocaml/coq/theories/Arith/Le.vos
 lib/ocaml/coq/theories/Arith/Lt.glob
 lib/ocaml/coq/theories/Arith/Lt.v
 lib/ocaml/coq/theories/Arith/Lt.vo
+lib/ocaml/coq/theories/Arith/Lt.vos
 lib/ocaml/coq/theories/Arith/Max.glob
 lib/ocaml/coq/theories/Arith/Max.v
 lib/ocaml/coq/theories/Arith/Max.vo
+lib/ocaml/coq/theories/Arith/Max.vos
 lib/ocaml/coq/theories/Arith/Min.glob
 lib/ocaml/coq/theories/Arith/Min.v
 lib/ocaml/coq/theories/Arith/Min.vo
+lib/ocaml/coq/theories/Arith/Min.vos
 lib/ocaml/coq/theories/Arith/Minus.glob
 lib/ocaml/coq/theories/Arith/Minus.v
 lib/ocaml/coq/theories/Arith/Minus.vo
+lib/ocaml/coq/theories/Arith/Minus.vos
 lib/ocaml/coq/theories/Arith/Mult.glob
 lib/ocaml/coq/theories/Arith/Mult.v
 lib/ocaml/coq/theories/Arith/Mult.vo
+lib/ocaml/coq/theories/Arith/Mult.vos
 lib/ocaml/coq/theories/Arith/PeanoNat.glob
 lib/ocaml/coq/theories/Arith/PeanoNat.v
 lib/ocaml/coq/theories/Arith/PeanoNat.vo
+lib/ocaml/coq/theories/Arith/PeanoNat.vos
 lib/ocaml/coq/theories/Arith/Peano_dec.glob
 lib/ocaml/coq/theories/Arith/Peano_dec.v
 lib/ocaml/coq/theories/Arith/Peano_dec.vo
+lib/ocaml/coq/theories/Arith/Peano_dec.vos
 lib/ocaml/coq/theories/Arith/Plus.glob
 lib/ocaml/coq/theories/Arith/Plus.v
 lib/ocaml/coq/theories/Arith/Plus.vo
+lib/ocaml/coq/theories/Arith/Plus.vos
 lib/ocaml/coq/theories/Arith/Wf_nat.glob
 lib/ocaml/coq/theories/Arith/Wf_nat.v
 lib/ocaml/coq/theories/Arith/Wf_nat.vo
+lib/ocaml/coq/theories/Arith/Wf_nat.vos
 lib/ocaml/coq/theories/Bool/
 lib/ocaml/coq/theories/Bool/.coq-native/
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bool.cmi
@@ -914,24 +1078,31 @@
 lib/ocaml/coq/theories/Bool/Bool.glob
 lib/ocaml/coq/theories/Bool/Bool.v
 lib/ocaml/coq/theories/Bool/Bool.vo
+lib/ocaml/coq/theories/Bool/Bool.vos
 lib/ocaml/coq/theories/Bool/BoolEq.glob
 lib/ocaml/coq/theories/Bool/BoolEq.v
 lib/ocaml/coq/theories/Bool/BoolEq.vo
+lib/ocaml/coq/theories/Bool/BoolEq.vos
 lib/ocaml/coq/theories/Bool/Bvector.glob
 lib/ocaml/coq/theories/Bool/Bvector.v
 lib/ocaml/coq/theories/Bool/Bvector.vo
+lib/ocaml/coq/theories/Bool/Bvector.vos
 lib/ocaml/coq/theories/Bool/DecBool.glob
 lib/ocaml/coq/theories/Bool/DecBool.v
 lib/ocaml/coq/theories/Bool/DecBool.vo
+lib/ocaml/coq/theories/Bool/DecBool.vos
 lib/ocaml/coq/theories/Bool/IfProp.glob
 lib/ocaml/coq/theories/Bool/IfProp.v
 lib/ocaml/coq/theories/Bool/IfProp.vo
+lib/ocaml/coq/theories/Bool/IfProp.vos
 lib/ocaml/coq/theories/Bool/Sumbool.glob
 lib/ocaml/coq/theories/Bool/Sumbool.v
 lib/ocaml/coq/theories/Bool/Sumbool.vo
+lib/ocaml/coq/theories/Bool/Sumbool.vos
 lib/ocaml/coq/theories/Bool/Zerob.glob
 lib/ocaml/coq/theories/Bool/Zerob.v
 lib/ocaml/coq/theories/Bool/Zerob.vo
+lib/ocaml/coq/theories/Bool/Zerob.vos
 lib/ocaml/coq/theories/Classes/
 lib/ocaml/coq/theories/Classes/.coq-native/
 lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_CEquivalence.cmi
@@ -952,66 +1123,85 @@
 lib/ocaml/coq/theories/Classes/CEquivalence.glob
 lib/ocaml/coq/theories/Classes/CEquivalence.v
 lib/ocaml/coq/theories/Classes/CEquivalence.vo
+lib/ocaml/coq/theories/Classes/CEquivalence.vos
 lib/ocaml/coq/theories/Classes/CMorphisms.glob
 lib/ocaml/coq/theories/Classes/CMorphisms.v
 lib/ocaml/coq/theories/Classes/CMorphisms.vo
+lib/ocaml/coq/theories/Classes/CMorphisms.vos
 lib/ocaml/coq/theories/Classes/CRelationClasses.glob
 lib/ocaml/coq/theories/Classes/CRelationClasses.v
 lib/ocaml/coq/theories/Classes/CRelationClasses.vo
+lib/ocaml/coq/theories/Classes/CRelationClasses.vos
 lib/ocaml/coq/theories/Classes/DecidableClass.glob
 lib/ocaml/coq/theories/Classes/DecidableClass.v
 lib/ocaml/coq/theories/Classes/DecidableClass.vo
+lib/ocaml/coq/theories/Classes/DecidableClass.vos
 lib/ocaml/coq/theories/Classes/EquivDec.glob
 lib/ocaml/coq/theories/Classes/EquivDec.v
 lib/ocaml/coq/theories/Classes/EquivDec.vo
+lib/ocaml/coq/theories/Classes/EquivDec.vos
 lib/ocaml/coq/theories/Classes/Equivalence.glob
 lib/ocaml/coq/theories/Classes/Equivalence.v
 lib/ocaml/coq/theories/Classes/Equivalence.vo
+lib/ocaml/coq/theories/Classes/Equivalence.vos
 lib/ocaml/coq/theories/Classes/Init.glob
 lib/ocaml/coq/theories/Classes/Init.v
 lib/ocaml/coq/theories/Classes/Init.vo
+lib/ocaml/coq/theories/Classes/Init.vos
 lib/ocaml/coq/theories/Classes/Morphisms.glob
 lib/ocaml/coq/theories/Classes/Morphisms.v
 lib/ocaml/coq/theories/Classes/Morphisms.vo
+lib/ocaml/coq/theories/Classes/Morphisms.vos
 lib/ocaml/coq/theories/Classes/Morphisms_Prop.glob
 lib/ocaml/coq/theories/Classes/Morphisms_Prop.v
 lib/ocaml/coq/theories/Classes/Morphisms_Prop.vo
+lib/ocaml/coq/theories/Classes/Morphisms_Prop.vos
 lib/ocaml/coq/theories/Classes/Morphisms_Relations.glob
 lib/ocaml/coq/theories/Classes/Morphisms_Relations.v
 lib/ocaml/coq/theories/Classes/Morphisms_Relations.vo
+lib/ocaml/coq/theories/Classes/Morphisms_Relations.vos
 lib/ocaml/coq/theories/Classes/RelationClasses.glob
 lib/ocaml/coq/theories/Classes/RelationClasses.v
 lib/ocaml/coq/theories/Classes/RelationClasses.vo
+lib/ocaml/coq/theories/Classes/RelationClasses.vos
 lib/ocaml/coq/theories/Classes/RelationPairs.glob
 lib/ocaml/coq/theories/Classes/RelationPairs.v
 lib/ocaml/coq/theories/Classes/RelationPairs.vo
+lib/ocaml/coq/theories/Classes/RelationPairs.vos
 lib/ocaml/coq/theories/Classes/SetoidClass.glob
 lib/ocaml/coq/theories/Classes/SetoidClass.v
 lib/ocaml/coq/theories/Classes/SetoidClass.vo
+lib/ocaml/coq/theories/Classes/SetoidClass.vos
 lib/ocaml/coq/theories/Classes/SetoidDec.glob
 lib/ocaml/coq/theories/Classes/SetoidDec.v
 lib/ocaml/coq/theories/Classes/SetoidDec.vo
+lib/ocaml/coq/theories/Classes/SetoidDec.vos
 lib/ocaml/coq/theories/Classes/SetoidTactics.glob
 lib/ocaml/coq/theories/Classes/SetoidTactics.v
 lib/ocaml/coq/theories/Classes/SetoidTactics.vo
+lib/ocaml/coq/theories/Classes/SetoidTactics.vos
 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_Coq810.cmi
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmi
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.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/AdmitAxiom.vos
 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/Coq810.vos
+lib/ocaml/coq/theories/Compat/Coq811.glob
+lib/ocaml/coq/theories/Compat/Coq811.v
+lib/ocaml/coq/theories/Compat/Coq811.vo
+lib/ocaml/coq/theories/Compat/Coq811.vos
 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/Compat/Coq89.vos
 lib/ocaml/coq/theories/FSets/
 lib/ocaml/coq/theories/FSets/.coq-native/
 lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
@@ -1038,66 +1228,124 @@
 lib/ocaml/coq/theories/FSets/FMapAVL.glob
 lib/ocaml/coq/theories/FSets/FMapAVL.v
 lib/ocaml/coq/theories/FSets/FMapAVL.vo
+lib/ocaml/coq/theories/FSets/FMapAVL.vos
 lib/ocaml/coq/theories/FSets/FMapFacts.glob
 lib/ocaml/coq/theories/FSets/FMapFacts.v
 lib/ocaml/coq/theories/FSets/FMapFacts.vo
+lib/ocaml/coq/theories/FSets/FMapFacts.vos
 lib/ocaml/coq/theories/FSets/FMapFullAVL.glob
 lib/ocaml/coq/theories/FSets/FMapFullAVL.v
 lib/ocaml/coq/theories/FSets/FMapFullAVL.vo
+lib/ocaml/coq/theories/FSets/FMapFullAVL.vos
 lib/ocaml/coq/theories/FSets/FMapInterface.glob
 lib/ocaml/coq/theories/FSets/FMapInterface.v
 lib/ocaml/coq/theories/FSets/FMapInterface.vo
+lib/ocaml/coq/theories/FSets/FMapInterface.vos
 lib/ocaml/coq/theories/FSets/FMapList.glob
 lib/ocaml/coq/theories/FSets/FMapList.v
 lib/ocaml/coq/theories/FSets/FMapList.vo
+lib/ocaml/coq/theories/FSets/FMapList.vos
 lib/ocaml/coq/theories/FSets/FMapPositive.glob
 lib/ocaml/coq/theories/FSets/FMapPositive.v
 lib/ocaml/coq/theories/FSets/FMapPositive.vo
+lib/ocaml/coq/theories/FSets/FMapPositive.vos
 lib/ocaml/coq/theories/FSets/FMapWeakList.glob
 lib/ocaml/coq/theories/FSets/FMapWeakList.v
 lib/ocaml/coq/theories/FSets/FMapWeakList.vo
+lib/ocaml/coq/theories/FSets/FMapWeakList.vos
 lib/ocaml/coq/theories/FSets/FMaps.glob
 lib/ocaml/coq/theories/FSets/FMaps.v
 lib/ocaml/coq/theories/FSets/FMaps.vo
+lib/ocaml/coq/theories/FSets/FMaps.vos
 lib/ocaml/coq/theories/FSets/FSetAVL.glob
 lib/ocaml/coq/theories/FSets/FSetAVL.v
 lib/ocaml/coq/theories/FSets/FSetAVL.vo
+lib/ocaml/coq/theories/FSets/FSetAVL.vos
 lib/ocaml/coq/theories/FSets/FSetBridge.glob
 lib/ocaml/coq/theories/FSets/FSetBridge.v
 lib/ocaml/coq/theories/FSets/FSetBridge.vo
+lib/ocaml/coq/theories/FSets/FSetBridge.vos
 lib/ocaml/coq/theories/FSets/FSetCompat.glob
 lib/ocaml/coq/theories/FSets/FSetCompat.v
 lib/ocaml/coq/theories/FSets/FSetCompat.vo
+lib/ocaml/coq/theories/FSets/FSetCompat.vos
 lib/ocaml/coq/theories/FSets/FSetDecide.glob
 lib/ocaml/coq/theories/FSets/FSetDecide.v
 lib/ocaml/coq/theories/FSets/FSetDecide.vo
+lib/ocaml/coq/theories/FSets/FSetDecide.vos
 lib/ocaml/coq/theories/FSets/FSetEqProperties.glob
 lib/ocaml/coq/theories/FSets/FSetEqProperties.v
 lib/ocaml/coq/theories/FSets/FSetEqProperties.vo
+lib/ocaml/coq/theories/FSets/FSetEqProperties.vos
 lib/ocaml/coq/theories/FSets/FSetFacts.glob
 lib/ocaml/coq/theories/FSets/FSetFacts.v
 lib/ocaml/coq/theories/FSets/FSetFacts.vo
+lib/ocaml/coq/theories/FSets/FSetFacts.vos
 lib/ocaml/coq/theories/FSets/FSetInterface.glob
 lib/ocaml/coq/theories/FSets/FSetInterface.v
 lib/ocaml/coq/theories/FSets/FSetInterface.vo
+lib/ocaml/coq/theories/FSets/FSetInterface.vos
 lib/ocaml/coq/theories/FSets/FSetList.glob
 lib/ocaml/coq/theories/FSets/FSetList.v
 lib/ocaml/coq/theories/FSets/FSetList.vo
+lib/ocaml/coq/theories/FSets/FSetList.vos
 lib/ocaml/coq/theories/FSets/FSetPositive.glob
 lib/ocaml/coq/theories/FSets/FSetPositive.v
 lib/ocaml/coq/theories/FSets/FSetPositive.vo
+lib/ocaml/coq/theories/FSets/FSetPositive.vos
 lib/ocaml/coq/theories/FSets/FSetProperties.glob
 lib/ocaml/coq/theories/FSets/FSetProperties.v
 lib/ocaml/coq/theories/FSets/FSetProperties.vo
+lib/ocaml/coq/theories/FSets/FSetProperties.vos
 lib/ocaml/coq/theories/FSets/FSetToFiniteSet.glob
 lib/ocaml/coq/theories/FSets/FSetToFiniteSet.v
 lib/ocaml/coq/theories/FSets/FSetToFiniteSet.vo
+lib/ocaml/coq/theories/FSets/FSetToFiniteSet.vos
 lib/ocaml/coq/theories/FSets/FSetWeakList.glob
 lib/ocaml/coq/theories/FSets/FSetWeakList.v
 lib/ocaml/coq/theories/FSets/FSetWeakList.vo
+lib/ocaml/coq/theories/FSets/FSetWeakList.vos
 lib/ocaml/coq/theories/FSets/FSets.glob
 lib/ocaml/coq/theories/FSets/FSets.v
 lib/ocaml/coq/theories/FSets/FSets.vo
+lib/ocaml/coq/theories/FSets/FSets.vos
+lib/ocaml/coq/theories/Floats/
+lib/ocaml/coq/theories/Floats/.coq-native/
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatAxioms.cmi
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.cmi
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.cmi
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.cmi
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.cmi
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.cmi
+lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.cmi
+lib/ocaml/coq/theories/Floats/FloatAxioms.glob
+lib/ocaml/coq/theories/Floats/FloatAxioms.v
+lib/ocaml/coq/theories/Floats/FloatAxioms.vo
+lib/ocaml/coq/theories/Floats/FloatAxioms.vos
+lib/ocaml/coq/theories/Floats/FloatClass.glob
+lib/ocaml/coq/theories/Floats/FloatClass.v
+lib/ocaml/coq/theories/Floats/FloatClass.vo
+lib/ocaml/coq/theories/Floats/FloatClass.vos
+lib/ocaml/coq/theories/Floats/FloatLemmas.glob
+lib/ocaml/coq/theories/Floats/FloatLemmas.v
+lib/ocaml/coq/theories/Floats/FloatLemmas.vo
+lib/ocaml/coq/theories/Floats/FloatLemmas.vos
+lib/ocaml/coq/theories/Floats/FloatOps.glob
+lib/ocaml/coq/theories/Floats/FloatOps.v
+lib/ocaml/coq/theories/Floats/FloatOps.vo
+lib/ocaml/coq/theories/Floats/FloatOps.vos
+lib/ocaml/coq/theories/Floats/Floats.glob
+lib/ocaml/coq/theories/Floats/Floats.v
+lib/ocaml/coq/theories/Floats/Floats.vo
+lib/ocaml/coq/theories/Floats/Floats.vos
+lib/ocaml/coq/theories/Floats/PrimFloat.glob
+lib/ocaml/coq/theories/Floats/PrimFloat.v
+lib/ocaml/coq/theories/Floats/PrimFloat.vo
+lib/ocaml/coq/theories/Floats/PrimFloat.vos
+lib/ocaml/coq/theories/Floats/SpecFloat.glob
+lib/ocaml/coq/theories/Floats/SpecFloat.v
+lib/ocaml/coq/theories/Floats/SpecFloat.vo
+lib/ocaml/coq/theories/Floats/SpecFloat.vos
 lib/ocaml/coq/theories/Init/
 lib/ocaml/coq/theories/Init/.coq-native/
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmi
@@ -1116,42 +1364,55 @@
 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/Byte.vos
 lib/ocaml/coq/theories/Init/Datatypes.glob
 lib/ocaml/coq/theories/Init/Datatypes.v
 lib/ocaml/coq/theories/Init/Datatypes.vo
+lib/ocaml/coq/theories/Init/Datatypes.vos
 lib/ocaml/coq/theories/Init/Decimal.glob
 lib/ocaml/coq/theories/Init/Decimal.v
 lib/ocaml/coq/theories/Init/Decimal.vo
+lib/ocaml/coq/theories/Init/Decimal.vos
 lib/ocaml/coq/theories/Init/Logic.glob
 lib/ocaml/coq/theories/Init/Logic.v
 lib/ocaml/coq/theories/Init/Logic.vo
+lib/ocaml/coq/theories/Init/Logic.vos
 lib/ocaml/coq/theories/Init/Logic_Type.glob
 lib/ocaml/coq/theories/Init/Logic_Type.v
 lib/ocaml/coq/theories/Init/Logic_Type.vo
+lib/ocaml/coq/theories/Init/Logic_Type.vos
 lib/ocaml/coq/theories/Init/Nat.glob
 lib/ocaml/coq/theories/Init/Nat.v
 lib/ocaml/coq/theories/Init/Nat.vo
+lib/ocaml/coq/theories/Init/Nat.vos
 lib/ocaml/coq/theories/Init/Notations.glob
 lib/ocaml/coq/theories/Init/Notations.v
 lib/ocaml/coq/theories/Init/Notations.vo
+lib/ocaml/coq/theories/Init/Notations.vos
 lib/ocaml/coq/theories/Init/Peano.glob
 lib/ocaml/coq/theories/Init/Peano.v
 lib/ocaml/coq/theories/Init/Peano.vo
+lib/ocaml/coq/theories/Init/Peano.vos
 lib/ocaml/coq/theories/Init/Prelude.glob
 lib/ocaml/coq/theories/Init/Prelude.v
 lib/ocaml/coq/theories/Init/Prelude.vo
+lib/ocaml/coq/theories/Init/Prelude.vos
 lib/ocaml/coq/theories/Init/Specif.glob
 lib/ocaml/coq/theories/Init/Specif.v
 lib/ocaml/coq/theories/Init/Specif.vo
+lib/ocaml/coq/theories/Init/Specif.vos
 lib/ocaml/coq/theories/Init/Tactics.glob
 lib/ocaml/coq/theories/Init/Tactics.v
 lib/ocaml/coq/theories/Init/Tactics.vo
+lib/ocaml/coq/theories/Init/Tactics.vos
 lib/ocaml/coq/theories/Init/Tauto.glob
 lib/ocaml/coq/theories/Init/Tauto.v
 lib/ocaml/coq/theories/Init/Tauto.vo
+lib/ocaml/coq/theories/Init/Tauto.vos
 lib/ocaml/coq/theories/Init/Wf.glob
 lib/ocaml/coq/theories/Init/Wf.v
 lib/ocaml/coq/theories/Init/Wf.vo
+lib/ocaml/coq/theories/Init/Wf.vos
 lib/ocaml/coq/theories/Lists/
 lib/ocaml/coq/theories/Lists/.coq-native/
 lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_List.cmi
@@ -1165,27 +1426,35 @@
 lib/ocaml/coq/theories/Lists/List.glob
 lib/ocaml/coq/theories/Lists/List.v
 lib/ocaml/coq/theories/Lists/List.vo
+lib/ocaml/coq/theories/Lists/List.vos
 lib/ocaml/coq/theories/Lists/ListDec.glob
 lib/ocaml/coq/theories/Lists/ListDec.v
 lib/ocaml/coq/theories/Lists/ListDec.vo
+lib/ocaml/coq/theories/Lists/ListDec.vos
 lib/ocaml/coq/theories/Lists/ListSet.glob
 lib/ocaml/coq/theories/Lists/ListSet.v
 lib/ocaml/coq/theories/Lists/ListSet.vo
+lib/ocaml/coq/theories/Lists/ListSet.vos
 lib/ocaml/coq/theories/Lists/ListTactics.glob
 lib/ocaml/coq/theories/Lists/ListTactics.v
 lib/ocaml/coq/theories/Lists/ListTactics.vo
+lib/ocaml/coq/theories/Lists/ListTactics.vos
 lib/ocaml/coq/theories/Lists/SetoidList.glob
 lib/ocaml/coq/theories/Lists/SetoidList.v
 lib/ocaml/coq/theories/Lists/SetoidList.vo
+lib/ocaml/coq/theories/Lists/SetoidList.vos
 lib/ocaml/coq/theories/Lists/SetoidPermutation.glob
 lib/ocaml/coq/theories/Lists/SetoidPermutation.v
 lib/ocaml/coq/theories/Lists/SetoidPermutation.vo
+lib/ocaml/coq/theories/Lists/SetoidPermutation.vos
 lib/ocaml/coq/theories/Lists/StreamMemo.glob
 lib/ocaml/coq/theories/Lists/StreamMemo.v
 lib/ocaml/coq/theories/Lists/StreamMemo.vo
+lib/ocaml/coq/theories/Lists/StreamMemo.vos
 lib/ocaml/coq/theories/Lists/Streams.glob
 lib/ocaml/coq/theories/Lists/Streams.v
 lib/ocaml/coq/theories/Lists/Streams.vo
+lib/ocaml/coq/theories/Lists/Streams.vos
 lib/ocaml/coq/theories/Logic/
 lib/ocaml/coq/theories/Logic/.coq-native/
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Berardi.cmi
@@ -1210,6 +1479,7 @@
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmi
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FinFun.cmi
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.cmi
+lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.cmi
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.cmi
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_IndefiniteDescription.cmi
 lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_JMeq.cmi
@@ -1227,111 +1497,151 @@
 lib/ocaml/coq/theories/Logic/Berardi.glob
 lib/ocaml/coq/theories/Logic/Berardi.v
 lib/ocaml/coq/theories/Logic/Berardi.vo
+lib/ocaml/coq/theories/Logic/Berardi.vos
 lib/ocaml/coq/theories/Logic/ChoiceFacts.glob
 lib/ocaml/coq/theories/Logic/ChoiceFacts.v
 lib/ocaml/coq/theories/Logic/ChoiceFacts.vo
+lib/ocaml/coq/theories/Logic/ChoiceFacts.vos
 lib/ocaml/coq/theories/Logic/Classical.glob
 lib/ocaml/coq/theories/Logic/Classical.v
 lib/ocaml/coq/theories/Logic/Classical.vo
+lib/ocaml/coq/theories/Logic/Classical.vos
 lib/ocaml/coq/theories/Logic/ClassicalChoice.glob
 lib/ocaml/coq/theories/Logic/ClassicalChoice.v
 lib/ocaml/coq/theories/Logic/ClassicalChoice.vo
+lib/ocaml/coq/theories/Logic/ClassicalChoice.vos
 lib/ocaml/coq/theories/Logic/ClassicalDescription.glob
 lib/ocaml/coq/theories/Logic/ClassicalDescription.v
 lib/ocaml/coq/theories/Logic/ClassicalDescription.vo
+lib/ocaml/coq/theories/Logic/ClassicalDescription.vos
 lib/ocaml/coq/theories/Logic/ClassicalEpsilon.glob
 lib/ocaml/coq/theories/Logic/ClassicalEpsilon.v
 lib/ocaml/coq/theories/Logic/ClassicalEpsilon.vo
+lib/ocaml/coq/theories/Logic/ClassicalEpsilon.vos
 lib/ocaml/coq/theories/Logic/ClassicalFacts.glob
 lib/ocaml/coq/theories/Logic/ClassicalFacts.v
 lib/ocaml/coq/theories/Logic/ClassicalFacts.vo
+lib/ocaml/coq/theories/Logic/ClassicalFacts.vos
 lib/ocaml/coq/theories/Logic/ClassicalUniqueChoice.glob
 lib/ocaml/coq/theories/Logic/ClassicalUniqueChoice.v
 lib/ocaml/coq/theories/Logic/ClassicalUniqueChoice.vo
+lib/ocaml/coq/theories/Logic/ClassicalUniqueChoice.vos
 lib/ocaml/coq/theories/Logic/Classical_Pred_Type.glob
 lib/ocaml/coq/theories/Logic/Classical_Pred_Type.v
 lib/ocaml/coq/theories/Logic/Classical_Pred_Type.vo
+lib/ocaml/coq/theories/Logic/Classical_Pred_Type.vos
 lib/ocaml/coq/theories/Logic/Classical_Prop.glob
 lib/ocaml/coq/theories/Logic/Classical_Prop.v
 lib/ocaml/coq/theories/Logic/Classical_Prop.vo
+lib/ocaml/coq/theories/Logic/Classical_Prop.vos
 lib/ocaml/coq/theories/Logic/ConstructiveEpsilon.glob
 lib/ocaml/coq/theories/Logic/ConstructiveEpsilon.v
 lib/ocaml/coq/theories/Logic/ConstructiveEpsilon.vo
+lib/ocaml/coq/theories/Logic/ConstructiveEpsilon.vos
 lib/ocaml/coq/theories/Logic/Decidable.glob
 lib/ocaml/coq/theories/Logic/Decidable.v
 lib/ocaml/coq/theories/Logic/Decidable.vo
+lib/ocaml/coq/theories/Logic/Decidable.vos
 lib/ocaml/coq/theories/Logic/Description.glob
 lib/ocaml/coq/theories/Logic/Description.v
 lib/ocaml/coq/theories/Logic/Description.vo
+lib/ocaml/coq/theories/Logic/Description.vos
 lib/ocaml/coq/theories/Logic/Diaconescu.glob
 lib/ocaml/coq/theories/Logic/Diaconescu.v
 lib/ocaml/coq/theories/Logic/Diaconescu.vo
+lib/ocaml/coq/theories/Logic/Diaconescu.vos
 lib/ocaml/coq/theories/Logic/Epsilon.glob
 lib/ocaml/coq/theories/Logic/Epsilon.v
 lib/ocaml/coq/theories/Logic/Epsilon.vo
+lib/ocaml/coq/theories/Logic/Epsilon.vos
 lib/ocaml/coq/theories/Logic/Eqdep.glob
 lib/ocaml/coq/theories/Logic/Eqdep.v
 lib/ocaml/coq/theories/Logic/Eqdep.vo
+lib/ocaml/coq/theories/Logic/Eqdep.vos
 lib/ocaml/coq/theories/Logic/EqdepFacts.glob
 lib/ocaml/coq/theories/Logic/EqdepFacts.v
 lib/ocaml/coq/theories/Logic/EqdepFacts.vo
+lib/ocaml/coq/theories/Logic/EqdepFacts.vos
 lib/ocaml/coq/theories/Logic/Eqdep_dec.glob
 lib/ocaml/coq/theories/Logic/Eqdep_dec.v
 lib/ocaml/coq/theories/Logic/Eqdep_dec.vo
+lib/ocaml/coq/theories/Logic/Eqdep_dec.vos
 lib/ocaml/coq/theories/Logic/ExtensionalFunctionRepresentative.glob
 lib/ocaml/coq/theories/Logic/ExtensionalFunctionRepresentative.v
 lib/ocaml/coq/theories/Logic/ExtensionalFunctionRepresentative.vo
+lib/ocaml/coq/theories/Logic/ExtensionalFunctionRepresentative.vos
 lib/ocaml/coq/theories/Logic/ExtensionalityFacts.glob
 lib/ocaml/coq/theories/Logic/ExtensionalityFacts.v
 lib/ocaml/coq/theories/Logic/ExtensionalityFacts.vo
+lib/ocaml/coq/theories/Logic/ExtensionalityFacts.vos
 lib/ocaml/coq/theories/Logic/FinFun.glob
 lib/ocaml/coq/theories/Logic/FinFun.v
 lib/ocaml/coq/theories/Logic/FinFun.vo
+lib/ocaml/coq/theories/Logic/FinFun.vos
 lib/ocaml/coq/theories/Logic/FunctionalExtensionality.glob
 lib/ocaml/coq/theories/Logic/FunctionalExtensionality.v
 lib/ocaml/coq/theories/Logic/FunctionalExtensionality.vo
+lib/ocaml/coq/theories/Logic/FunctionalExtensionality.vos
+lib/ocaml/coq/theories/Logic/HLevels.glob
+lib/ocaml/coq/theories/Logic/HLevels.v
+lib/ocaml/coq/theories/Logic/HLevels.vo
+lib/ocaml/coq/theories/Logic/HLevels.vos
 lib/ocaml/coq/theories/Logic/Hurkens.glob
 lib/ocaml/coq/theories/Logic/Hurkens.v
 lib/ocaml/coq/theories/Logic/Hurkens.vo
+lib/ocaml/coq/theories/Logic/Hurkens.vos
 lib/ocaml/coq/theories/Logic/IndefiniteDescription.glob
 lib/ocaml/coq/theories/Logic/IndefiniteDescription.v
 lib/ocaml/coq/theories/Logic/IndefiniteDescription.vo
+lib/ocaml/coq/theories/Logic/IndefiniteDescription.vos
 lib/ocaml/coq/theories/Logic/JMeq.glob
 lib/ocaml/coq/theories/Logic/JMeq.v
 lib/ocaml/coq/theories/Logic/JMeq.vo
+lib/ocaml/coq/theories/Logic/JMeq.vos
 lib/ocaml/coq/theories/Logic/ProofIrrelevance.glob
 lib/ocaml/coq/theories/Logic/ProofIrrelevance.v
 lib/ocaml/coq/theories/Logic/ProofIrrelevance.vo
+lib/ocaml/coq/theories/Logic/ProofIrrelevance.vos
 lib/ocaml/coq/theories/Logic/ProofIrrelevanceFacts.glob
 lib/ocaml/coq/theories/Logic/ProofIrrelevanceFacts.v
 lib/ocaml/coq/theories/Logic/ProofIrrelevanceFacts.vo
+lib/ocaml/coq/theories/Logic/ProofIrrelevanceFacts.vos
 lib/ocaml/coq/theories/Logic/PropExtensionality.glob
 lib/ocaml/coq/theories/Logic/PropExtensionality.v
 lib/ocaml/coq/theories/Logic/PropExtensionality.vo
+lib/ocaml/coq/theories/Logic/PropExtensionality.vos
 lib/ocaml/coq/theories/Logic/PropExtensionalityFacts.glob
 lib/ocaml/coq/theories/Logic/PropExtensionalityFacts.v
 lib/ocaml/coq/theories/Logic/PropExtensionalityFacts.vo
+lib/ocaml/coq/theories/Logic/PropExtensionalityFacts.vos
 lib/ocaml/coq/theories/Logic/PropFacts.glob
 lib/ocaml/coq/theories/Logic/PropFacts.v
 lib/ocaml/coq/theories/Logic/PropFacts.vo
+lib/ocaml/coq/theories/Logic/PropFacts.vos
 lib/ocaml/coq/theories/Logic/RelationalChoice.glob
 lib/ocaml/coq/theories/Logic/RelationalChoice.v
 lib/ocaml/coq/theories/Logic/RelationalChoice.vo
+lib/ocaml/coq/theories/Logic/RelationalChoice.vos
 lib/ocaml/coq/theories/Logic/SetIsType.glob
 lib/ocaml/coq/theories/Logic/SetIsType.v
 lib/ocaml/coq/theories/Logic/SetIsType.vo
+lib/ocaml/coq/theories/Logic/SetIsType.vos
 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/SetoidChoice.vos
 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/StrictProp.vos
 lib/ocaml/coq/theories/Logic/WKL.glob
 lib/ocaml/coq/theories/Logic/WKL.v
 lib/ocaml/coq/theories/Logic/WKL.vo
+lib/ocaml/coq/theories/Logic/WKL.vos
 lib/ocaml/coq/theories/Logic/WeakFan.glob
 lib/ocaml/coq/theories/Logic/WeakFan.v
 lib/ocaml/coq/theories/Logic/WeakFan.vo
+lib/ocaml/coq/theories/Logic/WeakFan.vos
 lib/ocaml/coq/theories/MSets/
 lib/ocaml/coq/theories/MSets/.coq-native/
 lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetAVL.cmi
@@ -1350,42 +1660,55 @@
 lib/ocaml/coq/theories/MSets/MSetAVL.glob
 lib/ocaml/coq/theories/MSets/MSetAVL.v
 lib/ocaml/coq/theories/MSets/MSetAVL.vo
+lib/ocaml/coq/theories/MSets/MSetAVL.vos
 lib/ocaml/coq/theories/MSets/MSetDecide.glob
 lib/ocaml/coq/theories/MSets/MSetDecide.v
 lib/ocaml/coq/theories/MSets/MSetDecide.vo
+lib/ocaml/coq/theories/MSets/MSetDecide.vos
 lib/ocaml/coq/theories/MSets/MSetEqProperties.glob
 lib/ocaml/coq/theories/MSets/MSetEqProperties.v
 lib/ocaml/coq/theories/MSets/MSetEqProperties.vo
+lib/ocaml/coq/theories/MSets/MSetEqProperties.vos
 lib/ocaml/coq/theories/MSets/MSetFacts.glob
 lib/ocaml/coq/theories/MSets/MSetFacts.v
 lib/ocaml/coq/theories/MSets/MSetFacts.vo
+lib/ocaml/coq/theories/MSets/MSetFacts.vos
 lib/ocaml/coq/theories/MSets/MSetGenTree.glob
 lib/ocaml/coq/theories/MSets/MSetGenTree.v
 lib/ocaml/coq/theories/MSets/MSetGenTree.vo
+lib/ocaml/coq/theories/MSets/MSetGenTree.vos
 lib/ocaml/coq/theories/MSets/MSetInterface.glob
 lib/ocaml/coq/theories/MSets/MSetInterface.v
 lib/ocaml/coq/theories/MSets/MSetInterface.vo
+lib/ocaml/coq/theories/MSets/MSetInterface.vos
 lib/ocaml/coq/theories/MSets/MSetList.glob
 lib/ocaml/coq/theories/MSets/MSetList.v
 lib/ocaml/coq/theories/MSets/MSetList.vo
+lib/ocaml/coq/theories/MSets/MSetList.vos
 lib/ocaml/coq/theories/MSets/MSetPositive.glob
 lib/ocaml/coq/theories/MSets/MSetPositive.v
 lib/ocaml/coq/theories/MSets/MSetPositive.vo
+lib/ocaml/coq/theories/MSets/MSetPositive.vos
 lib/ocaml/coq/theories/MSets/MSetProperties.glob
 lib/ocaml/coq/theories/MSets/MSetProperties.v
 lib/ocaml/coq/theories/MSets/MSetProperties.vo
+lib/ocaml/coq/theories/MSets/MSetProperties.vos
 lib/ocaml/coq/theories/MSets/MSetRBT.glob
 lib/ocaml/coq/theories/MSets/MSetRBT.v
 lib/ocaml/coq/theories/MSets/MSetRBT.vo
+lib/ocaml/coq/theories/MSets/MSetRBT.vos
 lib/ocaml/coq/theories/MSets/MSetToFiniteSet.glob
 lib/ocaml/coq/theories/MSets/MSetToFiniteSet.v
 lib/ocaml/coq/theories/MSets/MSetToFiniteSet.vo
+lib/ocaml/coq/theories/MSets/MSetToFiniteSet.vos
 lib/ocaml/coq/theories/MSets/MSetWeakList.glob
 lib/ocaml/coq/theories/MSets/MSetWeakList.v
 lib/ocaml/coq/theories/MSets/MSetWeakList.vo
+lib/ocaml/coq/theories/MSets/MSetWeakList.vos
 lib/ocaml/coq/theories/MSets/MSets.glob
 lib/ocaml/coq/theories/MSets/MSets.v
 lib/ocaml/coq/theories/MSets/MSets.vo
+lib/ocaml/coq/theories/MSets/MSets.vos
 lib/ocaml/coq/theories/NArith/
 lib/ocaml/coq/theories/NArith/.coq-native/
 lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_BinNat.cmi
@@ -1401,33 +1724,43 @@
 lib/ocaml/coq/theories/NArith/BinNat.glob
 lib/ocaml/coq/theories/NArith/BinNat.v
 lib/ocaml/coq/theories/NArith/BinNat.vo
+lib/ocaml/coq/theories/NArith/BinNat.vos
 lib/ocaml/coq/theories/NArith/BinNatDef.glob
 lib/ocaml/coq/theories/NArith/BinNatDef.v
 lib/ocaml/coq/theories/NArith/BinNatDef.vo
+lib/ocaml/coq/theories/NArith/BinNatDef.vos
 lib/ocaml/coq/theories/NArith/NArith.glob
 lib/ocaml/coq/theories/NArith/NArith.v
 lib/ocaml/coq/theories/NArith/NArith.vo
+lib/ocaml/coq/theories/NArith/NArith.vos
 lib/ocaml/coq/theories/NArith/Ndec.glob
 lib/ocaml/coq/theories/NArith/Ndec.v
 lib/ocaml/coq/theories/NArith/Ndec.vo
+lib/ocaml/coq/theories/NArith/Ndec.vos
 lib/ocaml/coq/theories/NArith/Ndigits.glob
 lib/ocaml/coq/theories/NArith/Ndigits.v
 lib/ocaml/coq/theories/NArith/Ndigits.vo
+lib/ocaml/coq/theories/NArith/Ndigits.vos
 lib/ocaml/coq/theories/NArith/Ndist.glob
 lib/ocaml/coq/theories/NArith/Ndist.v
 lib/ocaml/coq/theories/NArith/Ndist.vo
+lib/ocaml/coq/theories/NArith/Ndist.vos
 lib/ocaml/coq/theories/NArith/Ndiv_def.glob
 lib/ocaml/coq/theories/NArith/Ndiv_def.v
 lib/ocaml/coq/theories/NArith/Ndiv_def.vo
+lib/ocaml/coq/theories/NArith/Ndiv_def.vos
 lib/ocaml/coq/theories/NArith/Ngcd_def.glob
 lib/ocaml/coq/theories/NArith/Ngcd_def.v
 lib/ocaml/coq/theories/NArith/Ngcd_def.vo
+lib/ocaml/coq/theories/NArith/Ngcd_def.vos
 lib/ocaml/coq/theories/NArith/Nnat.glob
 lib/ocaml/coq/theories/NArith/Nnat.v
 lib/ocaml/coq/theories/NArith/Nnat.vo
+lib/ocaml/coq/theories/NArith/Nnat.vos
 lib/ocaml/coq/theories/NArith/Nsqrt_def.glob
 lib/ocaml/coq/theories/NArith/Nsqrt_def.v
 lib/ocaml/coq/theories/NArith/Nsqrt_def.vo
+lib/ocaml/coq/theories/NArith/Nsqrt_def.vos
 lib/ocaml/coq/theories/Numbers/
 lib/ocaml/coq/theories/Numbers/.coq-native/
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmi
@@ -1443,9 +1776,11 @@
 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/AltBinNotations.vos
 lib/ocaml/coq/theories/Numbers/BinNums.glob
 lib/ocaml/coq/theories/Numbers/BinNums.v
 lib/ocaml/coq/theories/Numbers/BinNums.vo
+lib/ocaml/coq/theories/Numbers/BinNums.vos
 lib/ocaml/coq/theories/Numbers/Cyclic/
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/.coq-native/
@@ -1455,12 +1790,15 @@
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.glob
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
+lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vos
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/DoubleType.glob
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/DoubleType.v
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/DoubleType.vo
+lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/DoubleType.vos
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.glob
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.v
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
+lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vos
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmi
@@ -1469,12 +1807,15 @@
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Cyclic31.glob
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Cyclic31.v
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Cyclic31.vo
+lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Cyclic31.vos
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Int31.glob
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Int31.v
 lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Int31.vo
+lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Int31.vos
 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/Int31/Ring31.vos
 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
@@ -1483,36 +1824,46 @@
 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/Cyclic63.vos
 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/Int63.vos
 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/Int63/Ring63.vos
 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
 lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.glob
 lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.v
 lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vo
+lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vos
 lib/ocaml/coq/theories/Numbers/DecimalFacts.glob
 lib/ocaml/coq/theories/Numbers/DecimalFacts.v
 lib/ocaml/coq/theories/Numbers/DecimalFacts.vo
+lib/ocaml/coq/theories/Numbers/DecimalFacts.vos
 lib/ocaml/coq/theories/Numbers/DecimalN.glob
 lib/ocaml/coq/theories/Numbers/DecimalN.v
 lib/ocaml/coq/theories/Numbers/DecimalN.vo
+lib/ocaml/coq/theories/Numbers/DecimalN.vos
 lib/ocaml/coq/theories/Numbers/DecimalNat.glob
 lib/ocaml/coq/theories/Numbers/DecimalNat.v
 lib/ocaml/coq/theories/Numbers/DecimalNat.vo
+lib/ocaml/coq/theories/Numbers/DecimalNat.vos
 lib/ocaml/coq/theories/Numbers/DecimalPos.glob
 lib/ocaml/coq/theories/Numbers/DecimalPos.v
 lib/ocaml/coq/theories/Numbers/DecimalPos.vo
+lib/ocaml/coq/theories/Numbers/DecimalPos.vos
 lib/ocaml/coq/theories/Numbers/DecimalString.glob
 lib/ocaml/coq/theories/Numbers/DecimalString.v
 lib/ocaml/coq/theories/Numbers/DecimalString.vo
+lib/ocaml/coq/theories/Numbers/DecimalString.vos
 lib/ocaml/coq/theories/Numbers/DecimalZ.glob
 lib/ocaml/coq/theories/Numbers/DecimalZ.v
 lib/ocaml/coq/theories/Numbers/DecimalZ.vo
+lib/ocaml/coq/theories/Numbers/DecimalZ.vos
 lib/ocaml/coq/theories/Numbers/Integer/
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/
@@ -1537,72 +1888,93 @@
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAdd.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAdd.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAdd.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAdd.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAddOrder.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAddOrder.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAxioms.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAxioms.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAxioms.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZAxioms.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBase.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBase.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBase.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBase.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBits.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBits.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBits.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZBits.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivEucl.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivEucl.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivEucl.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivEucl.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivFloor.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivFloor.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivFloor.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivFloor.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZGcd.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZGcd.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZGcd.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZGcd.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLcm.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLcm.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLcm.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLcm.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLt.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLt.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLt.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZLt.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMaxMin.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMaxMin.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMaxMin.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMaxMin.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMul.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMul.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMul.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMul.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMulOrder.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMulOrder.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZParity.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZParity.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZParity.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZParity.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZPow.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZPow.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZPow.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZPow.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZProperties.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZProperties.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZProperties.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZProperties.vos
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.glob
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.v
 lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
+lib/ocaml/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vos
 lib/ocaml/coq/theories/Numbers/Integer/Binary/
 lib/ocaml/coq/theories/Numbers/Integer/Binary/.coq-native/
 lib/ocaml/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmi
 lib/ocaml/coq/theories/Numbers/Integer/Binary/ZBinary.glob
 lib/ocaml/coq/theories/Numbers/Integer/Binary/ZBinary.v
 lib/ocaml/coq/theories/Numbers/Integer/Binary/ZBinary.vo
+lib/ocaml/coq/theories/Numbers/Integer/Binary/ZBinary.vos
 lib/ocaml/coq/theories/Numbers/Integer/NatPairs/
 lib/ocaml/coq/theories/Numbers/Integer/NatPairs/.coq-native/
 lib/ocaml/coq/theories/Numbers/Integer/NatPairs/.coq-native/NCoq_Numbers_Integer_NatPairs_ZNatPairs.cmi
 lib/ocaml/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.glob
 lib/ocaml/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.v
 lib/ocaml/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vo
+lib/ocaml/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vos
 lib/ocaml/coq/theories/Numbers/NaryFunctions.glob
 lib/ocaml/coq/theories/Numbers/NaryFunctions.v
 lib/ocaml/coq/theories/Numbers/NaryFunctions.vo
+lib/ocaml/coq/theories/Numbers/NaryFunctions.vos
 lib/ocaml/coq/theories/Numbers/NatInt/
 lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/
 lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZAdd.cmi
@@ -1624,51 +1996,67 @@
 lib/ocaml/coq/theories/Numbers/NatInt/NZAdd.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZAdd.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZAdd.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZAdd.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZAddOrder.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZAddOrder.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZAddOrder.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZAddOrder.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZAxioms.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZAxioms.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZAxioms.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZAxioms.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZBase.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZBase.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZBase.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZBase.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZBits.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZBits.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZBits.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZBits.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZDiv.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZDiv.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZDiv.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZDiv.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZDomain.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZDomain.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZDomain.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZDomain.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZGcd.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZGcd.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZGcd.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZGcd.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZLog.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZLog.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZLog.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZLog.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZMul.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZMul.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZMul.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZMul.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZMulOrder.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZMulOrder.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZMulOrder.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZMulOrder.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZOrder.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZOrder.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZOrder.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZOrder.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZParity.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZParity.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZParity.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZParity.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZPow.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZPow.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZPow.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZPow.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZProperties.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZProperties.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZProperties.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZProperties.vos
 lib/ocaml/coq/theories/Numbers/NatInt/NZSqrt.glob
 lib/ocaml/coq/theories/Numbers/NatInt/NZSqrt.v
 lib/ocaml/coq/theories/Numbers/NatInt/NZSqrt.vo
+lib/ocaml/coq/theories/Numbers/NatInt/NZSqrt.vos
 lib/ocaml/coq/theories/Numbers/Natural/
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/
@@ -1695,78 +2083,101 @@
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAdd.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAdd.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAdd.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAdd.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAddOrder.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAddOrder.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAddOrder.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAddOrder.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAxioms.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAxioms.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAxioms.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NAxioms.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBase.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBase.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBase.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBase.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBits.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBits.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBits.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NBits.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDefOps.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDefOps.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDefOps.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDefOps.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDiv.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDiv.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDiv.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NDiv.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NGcd.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NGcd.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NGcd.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NGcd.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NIso.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NIso.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NIso.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NIso.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLcm.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLcm.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLcm.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLcm.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLog.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLog.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLog.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NLog.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMaxMin.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMaxMin.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMaxMin.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMaxMin.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMulOrder.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMulOrder.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NMulOrder.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NOrder.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NOrder.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NOrder.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NOrder.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NParity.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NParity.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NParity.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NParity.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NPow.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NPow.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NPow.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NPow.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NProperties.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NProperties.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NProperties.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NProperties.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSqrt.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSqrt.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSqrt.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSqrt.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NStrongRec.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NStrongRec.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NStrongRec.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NStrongRec.vos
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSub.glob
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSub.v
 lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSub.vo
+lib/ocaml/coq/theories/Numbers/Natural/Abstract/NSub.vos
 lib/ocaml/coq/theories/Numbers/Natural/Binary/
 lib/ocaml/coq/theories/Numbers/Natural/Binary/.coq-native/
 lib/ocaml/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmi
 lib/ocaml/coq/theories/Numbers/Natural/Binary/NBinary.glob
 lib/ocaml/coq/theories/Numbers/Natural/Binary/NBinary.v
 lib/ocaml/coq/theories/Numbers/Natural/Binary/NBinary.vo
+lib/ocaml/coq/theories/Numbers/Natural/Binary/NBinary.vos
 lib/ocaml/coq/theories/Numbers/Natural/Peano/
 lib/ocaml/coq/theories/Numbers/Natural/Peano/.coq-native/
 lib/ocaml/coq/theories/Numbers/Natural/Peano/.coq-native/NCoq_Numbers_Natural_Peano_NPeano.cmi
 lib/ocaml/coq/theories/Numbers/Natural/Peano/NPeano.glob
 lib/ocaml/coq/theories/Numbers/Natural/Peano/NPeano.v
 lib/ocaml/coq/theories/Numbers/Natural/Peano/NPeano.vo
+lib/ocaml/coq/theories/Numbers/Natural/Peano/NPeano.vos
 lib/ocaml/coq/theories/Numbers/NumPrelude.glob
 lib/ocaml/coq/theories/Numbers/NumPrelude.v
 lib/ocaml/coq/theories/Numbers/NumPrelude.vo
+lib/ocaml/coq/theories/Numbers/NumPrelude.vos
 lib/ocaml/coq/theories/PArith/
 lib/ocaml/coq/theories/PArith/.coq-native/
 lib/ocaml/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmi
@@ -1777,18 +2188,23 @@
 lib/ocaml/coq/theories/PArith/BinPos.glob
 lib/ocaml/coq/theories/PArith/BinPos.v
 lib/ocaml/coq/theories/PArith/BinPos.vo
+lib/ocaml/coq/theories/PArith/BinPos.vos
 lib/ocaml/coq/theories/PArith/BinPosDef.glob
 lib/ocaml/coq/theories/PArith/BinPosDef.v
 lib/ocaml/coq/theories/PArith/BinPosDef.vo
+lib/ocaml/coq/theories/PArith/BinPosDef.vos
 lib/ocaml/coq/theories/PArith/PArith.glob
 lib/ocaml/coq/theories/PArith/PArith.v
 lib/ocaml/coq/theories/PArith/PArith.vo
+lib/ocaml/coq/theories/PArith/PArith.vos
 lib/ocaml/coq/theories/PArith/POrderedType.glob
 lib/ocaml/coq/theories/PArith/POrderedType.v
 lib/ocaml/coq/theories/PArith/POrderedType.vo
+lib/ocaml/coq/theories/PArith/POrderedType.vos
 lib/ocaml/coq/theories/PArith/Pnat.glob
 lib/ocaml/coq/theories/PArith/Pnat.v
 lib/ocaml/coq/theories/PArith/Pnat.vo
+lib/ocaml/coq/theories/PArith/Pnat.vos
 lib/ocaml/coq/theories/Program/
 lib/ocaml/coq/theories/Program/.coq-native/
 lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Basics.cmi
@@ -1803,30 +2219,39 @@
 lib/ocaml/coq/theories/Program/Basics.glob
 lib/ocaml/coq/theories/Program/Basics.v
 lib/ocaml/coq/theories/Program/Basics.vo
+lib/ocaml/coq/theories/Program/Basics.vos
 lib/ocaml/coq/theories/Program/Combinators.glob
 lib/ocaml/coq/theories/Program/Combinators.v
 lib/ocaml/coq/theories/Program/Combinators.vo
+lib/ocaml/coq/theories/Program/Combinators.vos
 lib/ocaml/coq/theories/Program/Equality.glob
 lib/ocaml/coq/theories/Program/Equality.v
 lib/ocaml/coq/theories/Program/Equality.vo
+lib/ocaml/coq/theories/Program/Equality.vos
 lib/ocaml/coq/theories/Program/Program.glob
 lib/ocaml/coq/theories/Program/Program.v
 lib/ocaml/coq/theories/Program/Program.vo
+lib/ocaml/coq/theories/Program/Program.vos
 lib/ocaml/coq/theories/Program/Subset.glob
 lib/ocaml/coq/theories/Program/Subset.v
 lib/ocaml/coq/theories/Program/Subset.vo
+lib/ocaml/coq/theories/Program/Subset.vos
 lib/ocaml/coq/theories/Program/Syntax.glob
 lib/ocaml/coq/theories/Program/Syntax.v
 lib/ocaml/coq/theories/Program/Syntax.vo
+lib/ocaml/coq/theories/Program/Syntax.vos
 lib/ocaml/coq/theories/Program/Tactics.glob
 lib/ocaml/coq/theories/Program/Tactics.v
 lib/ocaml/coq/theories/Program/Tactics.vo
+lib/ocaml/coq/theories/Program/Tactics.vos
 lib/ocaml/coq/theories/Program/Utils.glob
 lib/ocaml/coq/theories/Program/Utils.v
 lib/ocaml/coq/theories/Program/Utils.vo
+lib/ocaml/coq/theories/Program/Utils.vos
 lib/ocaml/coq/theories/Program/Wf.glob
 lib/ocaml/coq/theories/Program/Wf.v
 lib/ocaml/coq/theories/Program/Wf.vo
+lib/ocaml/coq/theories/Program/Wf.vos
 lib/ocaml/coq/theories/QArith/
 lib/ocaml/coq/theories/QArith/.coq-native/
 lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_QArith.cmi
@@ -1845,42 +2270,55 @@
 lib/ocaml/coq/theories/QArith/QArith.glob
 lib/ocaml/coq/theories/QArith/QArith.v
 lib/ocaml/coq/theories/QArith/QArith.vo
+lib/ocaml/coq/theories/QArith/QArith.vos
 lib/ocaml/coq/theories/QArith/QArith_base.glob
 lib/ocaml/coq/theories/QArith/QArith_base.v
 lib/ocaml/coq/theories/QArith/QArith_base.vo
+lib/ocaml/coq/theories/QArith/QArith_base.vos
 lib/ocaml/coq/theories/QArith/QOrderedType.glob
 lib/ocaml/coq/theories/QArith/QOrderedType.v
 lib/ocaml/coq/theories/QArith/QOrderedType.vo
+lib/ocaml/coq/theories/QArith/QOrderedType.vos
 lib/ocaml/coq/theories/QArith/Qabs.glob
 lib/ocaml/coq/theories/QArith/Qabs.v
 lib/ocaml/coq/theories/QArith/Qabs.vo
+lib/ocaml/coq/theories/QArith/Qabs.vos
 lib/ocaml/coq/theories/QArith/Qcabs.glob
 lib/ocaml/coq/theories/QArith/Qcabs.v
 lib/ocaml/coq/theories/QArith/Qcabs.vo
+lib/ocaml/coq/theories/QArith/Qcabs.vos
 lib/ocaml/coq/theories/QArith/Qcanon.glob
 lib/ocaml/coq/theories/QArith/Qcanon.v
 lib/ocaml/coq/theories/QArith/Qcanon.vo
+lib/ocaml/coq/theories/QArith/Qcanon.vos
 lib/ocaml/coq/theories/QArith/Qfield.glob
 lib/ocaml/coq/theories/QArith/Qfield.v
 lib/ocaml/coq/theories/QArith/Qfield.vo
+lib/ocaml/coq/theories/QArith/Qfield.vos
 lib/ocaml/coq/theories/QArith/Qminmax.glob
 lib/ocaml/coq/theories/QArith/Qminmax.v
 lib/ocaml/coq/theories/QArith/Qminmax.vo
+lib/ocaml/coq/theories/QArith/Qminmax.vos
 lib/ocaml/coq/theories/QArith/Qpower.glob
 lib/ocaml/coq/theories/QArith/Qpower.v
 lib/ocaml/coq/theories/QArith/Qpower.vo
+lib/ocaml/coq/theories/QArith/Qpower.vos
 lib/ocaml/coq/theories/QArith/Qreals.glob
 lib/ocaml/coq/theories/QArith/Qreals.v
 lib/ocaml/coq/theories/QArith/Qreals.vo
+lib/ocaml/coq/theories/QArith/Qreals.vos
 lib/ocaml/coq/theories/QArith/Qreduction.glob
 lib/ocaml/coq/theories/QArith/Qreduction.v
 lib/ocaml/coq/theories/QArith/Qreduction.vo
+lib/ocaml/coq/theories/QArith/Qreduction.vos
 lib/ocaml/coq/theories/QArith/Qring.glob
 lib/ocaml/coq/theories/QArith/Qring.v
 lib/ocaml/coq/theories/QArith/Qring.vo
+lib/ocaml/coq/theories/QArith/Qring.vos
 lib/ocaml/coq/theories/QArith/Qround.glob
 lib/ocaml/coq/theories/QArith/Qround.v
 lib/ocaml/coq/theories/QArith/Qround.vo
+lib/ocaml/coq/theories/QArith/Qround.vos
 lib/ocaml/coq/theories/Reals/
 lib/ocaml/coq/theories/Reals/.coq-native/
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Alembert.cmi
@@ -1888,6 +2326,13 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ArithProp.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_rel.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_DiscrR.cmi
@@ -1929,6 +2374,7 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpow_def.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpower.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsigma.cmi
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsqrt_def.cmi
@@ -1949,192 +2395,287 @@
 lib/ocaml/coq/theories/Reals/Alembert.glob
 lib/ocaml/coq/theories/Reals/Alembert.v
 lib/ocaml/coq/theories/Reals/Alembert.vo
+lib/ocaml/coq/theories/Reals/Alembert.vos
 lib/ocaml/coq/theories/Reals/AltSeries.glob
 lib/ocaml/coq/theories/Reals/AltSeries.v
 lib/ocaml/coq/theories/Reals/AltSeries.vo
+lib/ocaml/coq/theories/Reals/AltSeries.vos
 lib/ocaml/coq/theories/Reals/ArithProp.glob
 lib/ocaml/coq/theories/Reals/ArithProp.v
 lib/ocaml/coq/theories/Reals/ArithProp.vo
+lib/ocaml/coq/theories/Reals/ArithProp.vos
 lib/ocaml/coq/theories/Reals/Binomial.glob
 lib/ocaml/coq/theories/Reals/Binomial.v
 lib/ocaml/coq/theories/Reals/Binomial.vo
+lib/ocaml/coq/theories/Reals/Binomial.vos
 lib/ocaml/coq/theories/Reals/Cauchy_prod.glob
 lib/ocaml/coq/theories/Reals/Cauchy_prod.v
 lib/ocaml/coq/theories/Reals/Cauchy_prod.vo
+lib/ocaml/coq/theories/Reals/Cauchy_prod.vos
+lib/ocaml/coq/theories/Reals/ClassicalDedekindReals.glob
+lib/ocaml/coq/theories/Reals/ClassicalDedekindReals.v
+lib/ocaml/coq/theories/Reals/ClassicalDedekindReals.vo
+lib/ocaml/coq/theories/Reals/ClassicalDedekindReals.vos
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyReals.glob
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyReals.v
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyReals.vo
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyReals.vos
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyRealsMult.glob
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyRealsMult.v
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyRealsMult.vo
+lib/ocaml/coq/theories/Reals/ConstructiveCauchyRealsMult.vos
+lib/ocaml/coq/theories/Reals/ConstructiveRcomplete.glob
+lib/ocaml/coq/theories/Reals/ConstructiveRcomplete.v
+lib/ocaml/coq/theories/Reals/ConstructiveRcomplete.vo
+lib/ocaml/coq/theories/Reals/ConstructiveRcomplete.vos
+lib/ocaml/coq/theories/Reals/ConstructiveReals.glob
+lib/ocaml/coq/theories/Reals/ConstructiveReals.v
+lib/ocaml/coq/theories/Reals/ConstructiveReals.vo
+lib/ocaml/coq/theories/Reals/ConstructiveReals.vos
+lib/ocaml/coq/theories/Reals/ConstructiveRealsLUB.glob
+lib/ocaml/coq/theories/Reals/ConstructiveRealsLUB.v
+lib/ocaml/coq/theories/Reals/ConstructiveRealsLUB.vo
+lib/ocaml/coq/theories/Reals/ConstructiveRealsLUB.vos
+lib/ocaml/coq/theories/Reals/ConstructiveRealsMorphisms.glob
+lib/ocaml/coq/theories/Reals/ConstructiveRealsMorphisms.v
+lib/ocaml/coq/theories/Reals/ConstructiveRealsMorphisms.vo
+lib/ocaml/coq/theories/Reals/ConstructiveRealsMorphisms.vos
 lib/ocaml/coq/theories/Reals/Cos_plus.glob
 lib/ocaml/coq/theories/Reals/Cos_plus.v
 lib/ocaml/coq/theories/Reals/Cos_plus.vo
+lib/ocaml/coq/theories/Reals/Cos_plus.vos
 lib/ocaml/coq/theories/Reals/Cos_rel.glob
 lib/ocaml/coq/theories/Reals/Cos_rel.v
 lib/ocaml/coq/theories/Reals/Cos_rel.vo
+lib/ocaml/coq/theories/Reals/Cos_rel.vos
 lib/ocaml/coq/theories/Reals/DiscrR.glob
 lib/ocaml/coq/theories/Reals/DiscrR.v
 lib/ocaml/coq/theories/Reals/DiscrR.vo
+lib/ocaml/coq/theories/Reals/DiscrR.vos
 lib/ocaml/coq/theories/Reals/Exp_prop.glob
 lib/ocaml/coq/theories/Reals/Exp_prop.v
 lib/ocaml/coq/theories/Reals/Exp_prop.vo
+lib/ocaml/coq/theories/Reals/Exp_prop.vos
 lib/ocaml/coq/theories/Reals/Integration.glob
 lib/ocaml/coq/theories/Reals/Integration.v
 lib/ocaml/coq/theories/Reals/Integration.vo
+lib/ocaml/coq/theories/Reals/Integration.vos
 lib/ocaml/coq/theories/Reals/MVT.glob
 lib/ocaml/coq/theories/Reals/MVT.v
 lib/ocaml/coq/theories/Reals/MVT.vo
+lib/ocaml/coq/theories/Reals/MVT.vos
 lib/ocaml/coq/theories/Reals/Machin.glob
 lib/ocaml/coq/theories/Reals/Machin.v
 lib/ocaml/coq/theories/Reals/Machin.vo
+lib/ocaml/coq/theories/Reals/Machin.vos
 lib/ocaml/coq/theories/Reals/NewtonInt.glob
 lib/ocaml/coq/theories/Reals/NewtonInt.v
 lib/ocaml/coq/theories/Reals/NewtonInt.vo
+lib/ocaml/coq/theories/Reals/NewtonInt.vos
 lib/ocaml/coq/theories/Reals/PSeries_reg.glob
 lib/ocaml/coq/theories/Reals/PSeries_reg.v
 lib/ocaml/coq/theories/Reals/PSeries_reg.vo
+lib/ocaml/coq/theories/Reals/PSeries_reg.vos
 lib/ocaml/coq/theories/Reals/PartSum.glob
 lib/ocaml/coq/theories/Reals/PartSum.v
 lib/ocaml/coq/theories/Reals/PartSum.vo
+lib/ocaml/coq/theories/Reals/PartSum.vos
 lib/ocaml/coq/theories/Reals/RIneq.glob
 lib/ocaml/coq/theories/Reals/RIneq.v
 lib/ocaml/coq/theories/Reals/RIneq.vo
+lib/ocaml/coq/theories/Reals/RIneq.vos
 lib/ocaml/coq/theories/Reals/RList.glob
 lib/ocaml/coq/theories/Reals/RList.v
 lib/ocaml/coq/theories/Reals/RList.vo
+lib/ocaml/coq/theories/Reals/RList.vos
 lib/ocaml/coq/theories/Reals/ROrderedType.glob
 lib/ocaml/coq/theories/Reals/ROrderedType.v
 lib/ocaml/coq/theories/Reals/ROrderedType.vo
+lib/ocaml/coq/theories/Reals/ROrderedType.vos
 lib/ocaml/coq/theories/Reals/R_Ifp.glob
 lib/ocaml/coq/theories/Reals/R_Ifp.v
 lib/ocaml/coq/theories/Reals/R_Ifp.vo
+lib/ocaml/coq/theories/Reals/R_Ifp.vos
 lib/ocaml/coq/theories/Reals/R_sqr.glob
 lib/ocaml/coq/theories/Reals/R_sqr.v
 lib/ocaml/coq/theories/Reals/R_sqr.vo
+lib/ocaml/coq/theories/Reals/R_sqr.vos
 lib/ocaml/coq/theories/Reals/R_sqrt.glob
 lib/ocaml/coq/theories/Reals/R_sqrt.v
 lib/ocaml/coq/theories/Reals/R_sqrt.vo
+lib/ocaml/coq/theories/Reals/R_sqrt.vos
 lib/ocaml/coq/theories/Reals/Ranalysis.glob
 lib/ocaml/coq/theories/Reals/Ranalysis.v
 lib/ocaml/coq/theories/Reals/Ranalysis.vo
+lib/ocaml/coq/theories/Reals/Ranalysis.vos
 lib/ocaml/coq/theories/Reals/Ranalysis1.glob
 lib/ocaml/coq/theories/Reals/Ranalysis1.v
 lib/ocaml/coq/theories/Reals/Ranalysis1.vo
+lib/ocaml/coq/theories/Reals/Ranalysis1.vos
 lib/ocaml/coq/theories/Reals/Ranalysis2.glob
 lib/ocaml/coq/theories/Reals/Ranalysis2.v
 lib/ocaml/coq/theories/Reals/Ranalysis2.vo
+lib/ocaml/coq/theories/Reals/Ranalysis2.vos
 lib/ocaml/coq/theories/Reals/Ranalysis3.glob
 lib/ocaml/coq/theories/Reals/Ranalysis3.v
 lib/ocaml/coq/theories/Reals/Ranalysis3.vo
+lib/ocaml/coq/theories/Reals/Ranalysis3.vos
 lib/ocaml/coq/theories/Reals/Ranalysis4.glob
 lib/ocaml/coq/theories/Reals/Ranalysis4.v
 lib/ocaml/coq/theories/Reals/Ranalysis4.vo
+lib/ocaml/coq/theories/Reals/Ranalysis4.vos
 lib/ocaml/coq/theories/Reals/Ranalysis5.glob
 lib/ocaml/coq/theories/Reals/Ranalysis5.v
 lib/ocaml/coq/theories/Reals/Ranalysis5.vo
+lib/ocaml/coq/theories/Reals/Ranalysis5.vos
 lib/ocaml/coq/theories/Reals/Ranalysis_reg.glob
 lib/ocaml/coq/theories/Reals/Ranalysis_reg.v
 lib/ocaml/coq/theories/Reals/Ranalysis_reg.vo
+lib/ocaml/coq/theories/Reals/Ranalysis_reg.vos
 lib/ocaml/coq/theories/Reals/Ratan.glob
 lib/ocaml/coq/theories/Reals/Ratan.v
 lib/ocaml/coq/theories/Reals/Ratan.vo
+lib/ocaml/coq/theories/Reals/Ratan.vos
 lib/ocaml/coq/theories/Reals/Raxioms.glob
 lib/ocaml/coq/theories/Reals/Raxioms.v
 lib/ocaml/coq/theories/Reals/Raxioms.vo
+lib/ocaml/coq/theories/Reals/Raxioms.vos
 lib/ocaml/coq/theories/Reals/Rbase.glob
 lib/ocaml/coq/theories/Reals/Rbase.v
 lib/ocaml/coq/theories/Reals/Rbase.vo
+lib/ocaml/coq/theories/Reals/Rbase.vos
 lib/ocaml/coq/theories/Reals/Rbasic_fun.glob
 lib/ocaml/coq/theories/Reals/Rbasic_fun.v
 lib/ocaml/coq/theories/Reals/Rbasic_fun.vo
+lib/ocaml/coq/theories/Reals/Rbasic_fun.vos
 lib/ocaml/coq/theories/Reals/Rcomplete.glob
 lib/ocaml/coq/theories/Reals/Rcomplete.v
 lib/ocaml/coq/theories/Reals/Rcomplete.vo
+lib/ocaml/coq/theories/Reals/Rcomplete.vos
 lib/ocaml/coq/theories/Reals/Rdefinitions.glob
 lib/ocaml/coq/theories/Reals/Rdefinitions.v
 lib/ocaml/coq/theories/Reals/Rdefinitions.vo
+lib/ocaml/coq/theories/Reals/Rdefinitions.vos
 lib/ocaml/coq/theories/Reals/Rderiv.glob
 lib/ocaml/coq/theories/Reals/Rderiv.v
 lib/ocaml/coq/theories/Reals/Rderiv.vo
+lib/ocaml/coq/theories/Reals/Rderiv.vos
 lib/ocaml/coq/theories/Reals/Reals.glob
 lib/ocaml/coq/theories/Reals/Reals.v
 lib/ocaml/coq/theories/Reals/Reals.vo
+lib/ocaml/coq/theories/Reals/Reals.vos
 lib/ocaml/coq/theories/Reals/Rfunctions.glob
 lib/ocaml/coq/theories/Reals/Rfunctions.v
 lib/ocaml/coq/theories/Reals/Rfunctions.vo
+lib/ocaml/coq/theories/Reals/Rfunctions.vos
 lib/ocaml/coq/theories/Reals/Rgeom.glob
 lib/ocaml/coq/theories/Reals/Rgeom.v
 lib/ocaml/coq/theories/Reals/Rgeom.vo
+lib/ocaml/coq/theories/Reals/Rgeom.vos
 lib/ocaml/coq/theories/Reals/RiemannInt.glob
 lib/ocaml/coq/theories/Reals/RiemannInt.v
 lib/ocaml/coq/theories/Reals/RiemannInt.vo
+lib/ocaml/coq/theories/Reals/RiemannInt.vos
 lib/ocaml/coq/theories/Reals/RiemannInt_SF.glob
 lib/ocaml/coq/theories/Reals/RiemannInt_SF.v
 lib/ocaml/coq/theories/Reals/RiemannInt_SF.vo
+lib/ocaml/coq/theories/Reals/RiemannInt_SF.vos
 lib/ocaml/coq/theories/Reals/Rlimit.glob
 lib/ocaml/coq/theories/Reals/Rlimit.v
 lib/ocaml/coq/theories/Reals/Rlimit.vo
+lib/ocaml/coq/theories/Reals/Rlimit.vos
 lib/ocaml/coq/theories/Reals/Rlogic.glob
 lib/ocaml/coq/theories/Reals/Rlogic.v
 lib/ocaml/coq/theories/Reals/Rlogic.vo
+lib/ocaml/coq/theories/Reals/Rlogic.vos
 lib/ocaml/coq/theories/Reals/Rminmax.glob
 lib/ocaml/coq/theories/Reals/Rminmax.v
 lib/ocaml/coq/theories/Reals/Rminmax.vo
+lib/ocaml/coq/theories/Reals/Rminmax.vos
 lib/ocaml/coq/theories/Reals/Rpow_def.glob
 lib/ocaml/coq/theories/Reals/Rpow_def.v
 lib/ocaml/coq/theories/Reals/Rpow_def.vo
+lib/ocaml/coq/theories/Reals/Rpow_def.vos
 lib/ocaml/coq/theories/Reals/Rpower.glob
 lib/ocaml/coq/theories/Reals/Rpower.v
 lib/ocaml/coq/theories/Reals/Rpower.vo
+lib/ocaml/coq/theories/Reals/Rpower.vos
 lib/ocaml/coq/theories/Reals/Rprod.glob
 lib/ocaml/coq/theories/Reals/Rprod.v
 lib/ocaml/coq/theories/Reals/Rprod.vo
+lib/ocaml/coq/theories/Reals/Rprod.vos
+lib/ocaml/coq/theories/Reals/Rregisternames.glob
+lib/ocaml/coq/theories/Reals/Rregisternames.v
+lib/ocaml/coq/theories/Reals/Rregisternames.vo
+lib/ocaml/coq/theories/Reals/Rregisternames.vos
 lib/ocaml/coq/theories/Reals/Rseries.glob
 lib/ocaml/coq/theories/Reals/Rseries.v
 lib/ocaml/coq/theories/Reals/Rseries.vo
+lib/ocaml/coq/theories/Reals/Rseries.vos
 lib/ocaml/coq/theories/Reals/Rsigma.glob
 lib/ocaml/coq/theories/Reals/Rsigma.v
 lib/ocaml/coq/theories/Reals/Rsigma.vo
+lib/ocaml/coq/theories/Reals/Rsigma.vos
 lib/ocaml/coq/theories/Reals/Rsqrt_def.glob
 lib/ocaml/coq/theories/Reals/Rsqrt_def.v
 lib/ocaml/coq/theories/Reals/Rsqrt_def.vo
+lib/ocaml/coq/theories/Reals/Rsqrt_def.vos
 lib/ocaml/coq/theories/Reals/Rtopology.glob
 lib/ocaml/coq/theories/Reals/Rtopology.v
 lib/ocaml/coq/theories/Reals/Rtopology.vo
+lib/ocaml/coq/theories/Reals/Rtopology.vos
 lib/ocaml/coq/theories/Reals/Rtrigo.glob
 lib/ocaml/coq/theories/Reals/Rtrigo.v
 lib/ocaml/coq/theories/Reals/Rtrigo.vo
+lib/ocaml/coq/theories/Reals/Rtrigo.vos
 lib/ocaml/coq/theories/Reals/Rtrigo1.glob
 lib/ocaml/coq/theories/Reals/Rtrigo1.v
 lib/ocaml/coq/theories/Reals/Rtrigo1.vo
+lib/ocaml/coq/theories/Reals/Rtrigo1.vos
 lib/ocaml/coq/theories/Reals/Rtrigo_alt.glob
 lib/ocaml/coq/theories/Reals/Rtrigo_alt.v
 lib/ocaml/coq/theories/Reals/Rtrigo_alt.vo
+lib/ocaml/coq/theories/Reals/Rtrigo_alt.vos
 lib/ocaml/coq/theories/Reals/Rtrigo_calc.glob
 lib/ocaml/coq/theories/Reals/Rtrigo_calc.v
 lib/ocaml/coq/theories/Reals/Rtrigo_calc.vo
+lib/ocaml/coq/theories/Reals/Rtrigo_calc.vos
 lib/ocaml/coq/theories/Reals/Rtrigo_def.glob
 lib/ocaml/coq/theories/Reals/Rtrigo_def.v
 lib/ocaml/coq/theories/Reals/Rtrigo_def.vo
+lib/ocaml/coq/theories/Reals/Rtrigo_def.vos
 lib/ocaml/coq/theories/Reals/Rtrigo_fun.glob
 lib/ocaml/coq/theories/Reals/Rtrigo_fun.v
 lib/ocaml/coq/theories/Reals/Rtrigo_fun.vo
+lib/ocaml/coq/theories/Reals/Rtrigo_fun.vos
 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/Rtrigo_reg.vos
 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/Runcountable.vos
 lib/ocaml/coq/theories/Reals/SeqProp.glob
 lib/ocaml/coq/theories/Reals/SeqProp.v
 lib/ocaml/coq/theories/Reals/SeqProp.vo
+lib/ocaml/coq/theories/Reals/SeqProp.vos
 lib/ocaml/coq/theories/Reals/SeqSeries.glob
 lib/ocaml/coq/theories/Reals/SeqSeries.v
 lib/ocaml/coq/theories/Reals/SeqSeries.vo
+lib/ocaml/coq/theories/Reals/SeqSeries.vos
 lib/ocaml/coq/theories/Reals/SplitAbsolu.glob
 lib/ocaml/coq/theories/Reals/SplitAbsolu.v
 lib/ocaml/coq/theories/Reals/SplitAbsolu.vo
+lib/ocaml/coq/theories/Reals/SplitAbsolu.vos
 lib/ocaml/coq/theories/Reals/SplitRmult.glob
 lib/ocaml/coq/theories/Reals/SplitRmult.v
 lib/ocaml/coq/theories/Reals/SplitRmult.vo
+lib/ocaml/coq/theories/Reals/SplitRmult.vos
 lib/ocaml/coq/theories/Reals/Sqrt_reg.glob
 lib/ocaml/coq/theories/Reals/Sqrt_reg.v
 lib/ocaml/coq/theories/Reals/Sqrt_reg.vo
+lib/ocaml/coq/theories/Reals/Sqrt_reg.vos
 lib/ocaml/coq/theories/Relations/
 lib/ocaml/coq/theories/Relations/.coq-native/
 lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Operators_Properties.cmi
@@ -2144,21 +2685,26 @@
 lib/ocaml/coq/theories/Relations/Operators_Properties.glob
 lib/ocaml/coq/theories/Relations/Operators_Properties.v
 lib/ocaml/coq/theories/Relations/Operators_Properties.vo
+lib/ocaml/coq/theories/Relations/Operators_Properties.vos
 lib/ocaml/coq/theories/Relations/Relation_Definitions.glob
 lib/ocaml/coq/theories/Relations/Relation_Definitions.v
 lib/ocaml/coq/theories/Relations/Relation_Definitions.vo
+lib/ocaml/coq/theories/Relations/Relation_Definitions.vos
 lib/ocaml/coq/theories/Relations/Relation_Operators.glob
 lib/ocaml/coq/theories/Relations/Relation_Operators.v
 lib/ocaml/coq/theories/Relations/Relation_Operators.vo
+lib/ocaml/coq/theories/Relations/Relation_Operators.vos
 lib/ocaml/coq/theories/Relations/Relations.glob
 lib/ocaml/coq/theories/Relations/Relations.v
 lib/ocaml/coq/theories/Relations/Relations.vo
+lib/ocaml/coq/theories/Relations/Relations.vos
 lib/ocaml/coq/theories/Setoids/
 lib/ocaml/coq/theories/Setoids/.coq-native/
 lib/ocaml/coq/theories/Setoids/.coq-native/NCoq_Setoids_Setoid.cmi
 lib/ocaml/coq/theories/Setoids/Setoid.glob
 lib/ocaml/coq/theories/Setoids/Setoid.v
 lib/ocaml/coq/theories/Setoids/Setoid.vo
+lib/ocaml/coq/theories/Setoids/Setoid.vos
 lib/ocaml/coq/theories/Sets/
 lib/ocaml/coq/theories/Sets/.coq-native/
 lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Classical_sets.cmi
@@ -2186,69 +2732,91 @@
 lib/ocaml/coq/theories/Sets/Classical_sets.glob
 lib/ocaml/coq/theories/Sets/Classical_sets.v
 lib/ocaml/coq/theories/Sets/Classical_sets.vo
+lib/ocaml/coq/theories/Sets/Classical_sets.vos
 lib/ocaml/coq/theories/Sets/Constructive_sets.glob
 lib/ocaml/coq/theories/Sets/Constructive_sets.v
 lib/ocaml/coq/theories/Sets/Constructive_sets.vo
+lib/ocaml/coq/theories/Sets/Constructive_sets.vos
 lib/ocaml/coq/theories/Sets/Cpo.glob
 lib/ocaml/coq/theories/Sets/Cpo.v
 lib/ocaml/coq/theories/Sets/Cpo.vo
+lib/ocaml/coq/theories/Sets/Cpo.vos
 lib/ocaml/coq/theories/Sets/Ensembles.glob
 lib/ocaml/coq/theories/Sets/Ensembles.v
 lib/ocaml/coq/theories/Sets/Ensembles.vo
+lib/ocaml/coq/theories/Sets/Ensembles.vos
 lib/ocaml/coq/theories/Sets/Finite_sets.glob
 lib/ocaml/coq/theories/Sets/Finite_sets.v
 lib/ocaml/coq/theories/Sets/Finite_sets.vo
+lib/ocaml/coq/theories/Sets/Finite_sets.vos
 lib/ocaml/coq/theories/Sets/Finite_sets_facts.glob
 lib/ocaml/coq/theories/Sets/Finite_sets_facts.v
 lib/ocaml/coq/theories/Sets/Finite_sets_facts.vo
+lib/ocaml/coq/theories/Sets/Finite_sets_facts.vos
 lib/ocaml/coq/theories/Sets/Image.glob
 lib/ocaml/coq/theories/Sets/Image.v
 lib/ocaml/coq/theories/Sets/Image.vo
+lib/ocaml/coq/theories/Sets/Image.vos
 lib/ocaml/coq/theories/Sets/Infinite_sets.glob
 lib/ocaml/coq/theories/Sets/Infinite_sets.v
 lib/ocaml/coq/theories/Sets/Infinite_sets.vo
+lib/ocaml/coq/theories/Sets/Infinite_sets.vos
 lib/ocaml/coq/theories/Sets/Integers.glob
 lib/ocaml/coq/theories/Sets/Integers.v
 lib/ocaml/coq/theories/Sets/Integers.vo
+lib/ocaml/coq/theories/Sets/Integers.vos
 lib/ocaml/coq/theories/Sets/Multiset.glob
 lib/ocaml/coq/theories/Sets/Multiset.v
 lib/ocaml/coq/theories/Sets/Multiset.vo
+lib/ocaml/coq/theories/Sets/Multiset.vos
 lib/ocaml/coq/theories/Sets/Partial_Order.glob
 lib/ocaml/coq/theories/Sets/Partial_Order.v
 lib/ocaml/coq/theories/Sets/Partial_Order.vo
+lib/ocaml/coq/theories/Sets/Partial_Order.vos
 lib/ocaml/coq/theories/Sets/Permut.glob
 lib/ocaml/coq/theories/Sets/Permut.v
 lib/ocaml/coq/theories/Sets/Permut.vo
+lib/ocaml/coq/theories/Sets/Permut.vos
 lib/ocaml/coq/theories/Sets/Powerset.glob
 lib/ocaml/coq/theories/Sets/Powerset.v
 lib/ocaml/coq/theories/Sets/Powerset.vo
+lib/ocaml/coq/theories/Sets/Powerset.vos
 lib/ocaml/coq/theories/Sets/Powerset_Classical_facts.glob
 lib/ocaml/coq/theories/Sets/Powerset_Classical_facts.v
 lib/ocaml/coq/theories/Sets/Powerset_Classical_facts.vo
+lib/ocaml/coq/theories/Sets/Powerset_Classical_facts.vos
 lib/ocaml/coq/theories/Sets/Powerset_facts.glob
 lib/ocaml/coq/theories/Sets/Powerset_facts.v
 lib/ocaml/coq/theories/Sets/Powerset_facts.vo
+lib/ocaml/coq/theories/Sets/Powerset_facts.vos
 lib/ocaml/coq/theories/Sets/Relations_1.glob
 lib/ocaml/coq/theories/Sets/Relations_1.v
 lib/ocaml/coq/theories/Sets/Relations_1.vo
+lib/ocaml/coq/theories/Sets/Relations_1.vos
 lib/ocaml/coq/theories/Sets/Relations_1_facts.glob
 lib/ocaml/coq/theories/Sets/Relations_1_facts.v
 lib/ocaml/coq/theories/Sets/Relations_1_facts.vo
+lib/ocaml/coq/theories/Sets/Relations_1_facts.vos
 lib/ocaml/coq/theories/Sets/Relations_2.glob
 lib/ocaml/coq/theories/Sets/Relations_2.v
 lib/ocaml/coq/theories/Sets/Relations_2.vo
+lib/ocaml/coq/theories/Sets/Relations_2.vos
 lib/ocaml/coq/theories/Sets/Relations_2_facts.glob
 lib/ocaml/coq/theories/Sets/Relations_2_facts.v
 lib/ocaml/coq/theories/Sets/Relations_2_facts.vo
+lib/ocaml/coq/theories/Sets/Relations_2_facts.vos
 lib/ocaml/coq/theories/Sets/Relations_3.glob
 lib/ocaml/coq/theories/Sets/Relations_3.v
 lib/ocaml/coq/theories/Sets/Relations_3.vo
+lib/ocaml/coq/theories/Sets/Relations_3.vos
 lib/ocaml/coq/theories/Sets/Relations_3_facts.glob
 lib/ocaml/coq/theories/Sets/Relations_3_facts.v
 lib/ocaml/coq/theories/Sets/Relations_3_facts.vo
+lib/ocaml/coq/theories/Sets/Relations_3_facts.vos
 lib/ocaml/coq/theories/Sets/Uniset.glob
 lib/ocaml/coq/theories/Sets/Uniset.v
 lib/ocaml/coq/theories/Sets/Uniset.vo
+lib/ocaml/coq/theories/Sets/Uniset.vos
 lib/ocaml/coq/theories/Sorting/
 lib/ocaml/coq/theories/Sorting/.coq-native/
 lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.cmi
@@ -2261,24 +2829,31 @@
 lib/ocaml/coq/theories/Sorting/Heap.glob
 lib/ocaml/coq/theories/Sorting/Heap.v
 lib/ocaml/coq/theories/Sorting/Heap.vo
+lib/ocaml/coq/theories/Sorting/Heap.vos
 lib/ocaml/coq/theories/Sorting/Mergesort.glob
 lib/ocaml/coq/theories/Sorting/Mergesort.v
 lib/ocaml/coq/theories/Sorting/Mergesort.vo
+lib/ocaml/coq/theories/Sorting/Mergesort.vos
 lib/ocaml/coq/theories/Sorting/PermutEq.glob
 lib/ocaml/coq/theories/Sorting/PermutEq.v
 lib/ocaml/coq/theories/Sorting/PermutEq.vo
+lib/ocaml/coq/theories/Sorting/PermutEq.vos
 lib/ocaml/coq/theories/Sorting/PermutSetoid.glob
 lib/ocaml/coq/theories/Sorting/PermutSetoid.v
 lib/ocaml/coq/theories/Sorting/PermutSetoid.vo
+lib/ocaml/coq/theories/Sorting/PermutSetoid.vos
 lib/ocaml/coq/theories/Sorting/Permutation.glob
 lib/ocaml/coq/theories/Sorting/Permutation.v
 lib/ocaml/coq/theories/Sorting/Permutation.vo
+lib/ocaml/coq/theories/Sorting/Permutation.vos
 lib/ocaml/coq/theories/Sorting/Sorted.glob
 lib/ocaml/coq/theories/Sorting/Sorted.v
 lib/ocaml/coq/theories/Sorting/Sorted.vo
+lib/ocaml/coq/theories/Sorting/Sorted.vos
 lib/ocaml/coq/theories/Sorting/Sorting.glob
 lib/ocaml/coq/theories/Sorting/Sorting.v
 lib/ocaml/coq/theories/Sorting/Sorting.vo
+lib/ocaml/coq/theories/Sorting/Sorting.vos
 lib/ocaml/coq/theories/Strings/
 lib/ocaml/coq/theories/Strings/.coq-native/
 lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmi
@@ -2291,24 +2866,31 @@
 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/Ascii.vos
 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/BinaryString.vos
 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/Byte.vos
 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/ByteVector.vos
 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/HexString.vos
 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/OctalString.vos
 lib/ocaml/coq/theories/Strings/String.glob
 lib/ocaml/coq/theories/Strings/String.v
 lib/ocaml/coq/theories/Strings/String.vo
+lib/ocaml/coq/theories/Strings/String.vos
 lib/ocaml/coq/theories/Structures/
 lib/ocaml/coq/theories/Structures/.coq-native/
 lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableType.cmi
@@ -2328,45 +2910,59 @@
 lib/ocaml/coq/theories/Structures/DecidableType.glob
 lib/ocaml/coq/theories/Structures/DecidableType.v
 lib/ocaml/coq/theories/Structures/DecidableType.vo
+lib/ocaml/coq/theories/Structures/DecidableType.vos
 lib/ocaml/coq/theories/Structures/DecidableTypeEx.glob
 lib/ocaml/coq/theories/Structures/DecidableTypeEx.v
 lib/ocaml/coq/theories/Structures/DecidableTypeEx.vo
+lib/ocaml/coq/theories/Structures/DecidableTypeEx.vos
 lib/ocaml/coq/theories/Structures/Equalities.glob
 lib/ocaml/coq/theories/Structures/Equalities.v
 lib/ocaml/coq/theories/Structures/Equalities.vo
+lib/ocaml/coq/theories/Structures/Equalities.vos
 lib/ocaml/coq/theories/Structures/EqualitiesFacts.glob
 lib/ocaml/coq/theories/Structures/EqualitiesFacts.v
 lib/ocaml/coq/theories/Structures/EqualitiesFacts.vo
+lib/ocaml/coq/theories/Structures/EqualitiesFacts.vos
 lib/ocaml/coq/theories/Structures/GenericMinMax.glob
 lib/ocaml/coq/theories/Structures/GenericMinMax.v
 lib/ocaml/coq/theories/Structures/GenericMinMax.vo
+lib/ocaml/coq/theories/Structures/GenericMinMax.vos
 lib/ocaml/coq/theories/Structures/OrderedType.glob
 lib/ocaml/coq/theories/Structures/OrderedType.v
 lib/ocaml/coq/theories/Structures/OrderedType.vo
+lib/ocaml/coq/theories/Structures/OrderedType.vos
 lib/ocaml/coq/theories/Structures/OrderedTypeAlt.glob
 lib/ocaml/coq/theories/Structures/OrderedTypeAlt.v
 lib/ocaml/coq/theories/Structures/OrderedTypeAlt.vo
+lib/ocaml/coq/theories/Structures/OrderedTypeAlt.vos
 lib/ocaml/coq/theories/Structures/OrderedTypeEx.glob
 lib/ocaml/coq/theories/Structures/OrderedTypeEx.v
 lib/ocaml/coq/theories/Structures/OrderedTypeEx.vo
+lib/ocaml/coq/theories/Structures/OrderedTypeEx.vos
 lib/ocaml/coq/theories/Structures/Orders.glob
 lib/ocaml/coq/theories/Structures/Orders.v
 lib/ocaml/coq/theories/Structures/Orders.vo
+lib/ocaml/coq/theories/Structures/Orders.vos
 lib/ocaml/coq/theories/Structures/OrdersAlt.glob
 lib/ocaml/coq/theories/Structures/OrdersAlt.v
 lib/ocaml/coq/theories/Structures/OrdersAlt.vo
+lib/ocaml/coq/theories/Structures/OrdersAlt.vos
 lib/ocaml/coq/theories/Structures/OrdersEx.glob
 lib/ocaml/coq/theories/Structures/OrdersEx.v
 lib/ocaml/coq/theories/Structures/OrdersEx.vo
+lib/ocaml/coq/theories/Structures/OrdersEx.vos
 lib/ocaml/coq/theories/Structures/OrdersFacts.glob
 lib/ocaml/coq/theories/Structures/OrdersFacts.v
 lib/ocaml/coq/theories/Structures/OrdersFacts.vo
+lib/ocaml/coq/theories/Structures/OrdersFacts.vos
 lib/ocaml/coq/theories/Structures/OrdersLists.glob
 lib/ocaml/coq/theories/Structures/OrdersLists.v
 lib/ocaml/coq/theories/Structures/OrdersLists.vo
+lib/ocaml/coq/theories/Structures/OrdersLists.vos
 lib/ocaml/coq/theories/Structures/OrdersTac.glob
 lib/ocaml/coq/theories/Structures/OrdersTac.v
 lib/ocaml/coq/theories/Structures/OrdersTac.vo
+lib/ocaml/coq/theories/Structures/OrdersTac.vos
 lib/ocaml/coq/theories/Unicode/
 lib/ocaml/coq/theories/Unicode/.coq-native/
 lib/ocaml/coq/theories/Unicode/.coq-native/NCoq_Unicode_Utf8.cmi
@@ -2374,9 +2970,11 @@
 lib/ocaml/coq/theories/Unicode/Utf8.glob
 lib/ocaml/coq/theories/Unicode/Utf8.v
 lib/ocaml/coq/theories/Unicode/Utf8.vo
+lib/ocaml/coq/theories/Unicode/Utf8.vos
 lib/ocaml/coq/theories/Unicode/Utf8_core.glob
 lib/ocaml/coq/theories/Unicode/Utf8_core.v
 lib/ocaml/coq/theories/Unicode/Utf8_core.vo
+lib/ocaml/coq/theories/Unicode/Utf8_core.vos
 lib/ocaml/coq/theories/Vectors/
 lib/ocaml/coq/theories/Vectors/.coq-native/
 lib/ocaml/coq/theories/Vectors/.coq-native/NCoq_Vectors_Fin.cmi
@@ -2387,18 +2985,23 @@
 lib/ocaml/coq/theories/Vectors/Fin.glob
 lib/ocaml/coq/theories/Vectors/Fin.v
 lib/ocaml/coq/theories/Vectors/Fin.vo
+lib/ocaml/coq/theories/Vectors/Fin.vos
 lib/ocaml/coq/theories/Vectors/Vector.glob
 lib/ocaml/coq/theories/Vectors/Vector.v
 lib/ocaml/coq/theories/Vectors/Vector.vo
+lib/ocaml/coq/theories/Vectors/Vector.vos
 lib/ocaml/coq/theories/Vectors/VectorDef.glob
 lib/ocaml/coq/theories/Vectors/VectorDef.v
 lib/ocaml/coq/theories/Vectors/VectorDef.vo
+lib/ocaml/coq/theories/Vectors/VectorDef.vos
 lib/ocaml/coq/theories/Vectors/VectorEq.glob
 lib/ocaml/coq/theories/Vectors/VectorEq.v
 lib/ocaml/coq/theories/Vectors/VectorEq.vo
+lib/ocaml/coq/theories/Vectors/VectorEq.vos
 lib/ocaml/coq/theories/Vectors/VectorSpec.glob
 lib/ocaml/coq/theories/Vectors/VectorSpec.v
 lib/ocaml/coq/theories/Vectors/VectorSpec.vo
+lib/ocaml/coq/theories/Vectors/VectorSpec.vos
 lib/ocaml/coq/theories/Wellfounded/
 lib/ocaml/coq/theories/Wellfounded/.coq-native/
 lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Disjoint_Union.cmi
@@ -2413,30 +3016,39 @@
 lib/ocaml/coq/theories/Wellfounded/Disjoint_Union.glob
 lib/ocaml/coq/theories/Wellfounded/Disjoint_Union.v
 lib/ocaml/coq/theories/Wellfounded/Disjoint_Union.vo
+lib/ocaml/coq/theories/Wellfounded/Disjoint_Union.vos
 lib/ocaml/coq/theories/Wellfounded/Inclusion.glob
 lib/ocaml/coq/theories/Wellfounded/Inclusion.v
 lib/ocaml/coq/theories/Wellfounded/Inclusion.vo
+lib/ocaml/coq/theories/Wellfounded/Inclusion.vos
 lib/ocaml/coq/theories/Wellfounded/Inverse_Image.glob
 lib/ocaml/coq/theories/Wellfounded/Inverse_Image.v
 lib/ocaml/coq/theories/Wellfounded/Inverse_Image.vo
+lib/ocaml/coq/theories/Wellfounded/Inverse_Image.vos
 lib/ocaml/coq/theories/Wellfounded/Lexicographic_Exponentiation.glob
 lib/ocaml/coq/theories/Wellfounded/Lexicographic_Exponentiation.v
 lib/ocaml/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo
+lib/ocaml/coq/theories/Wellfounded/Lexicographic_Exponentiation.vos
 lib/ocaml/coq/theories/Wellfounded/Lexicographic_Product.glob
 lib/ocaml/coq/theories/Wellfounded/Lexicographic_Product.v
 lib/ocaml/coq/theories/Wellfounded/Lexicographic_Product.vo
+lib/ocaml/coq/theories/Wellfounded/Lexicographic_Product.vos
 lib/ocaml/coq/theories/Wellfounded/Transitive_Closure.glob
 lib/ocaml/coq/theories/Wellfounded/Transitive_Closure.v
 lib/ocaml/coq/theories/Wellfounded/Transitive_Closure.vo
+lib/ocaml/coq/theories/Wellfounded/Transitive_Closure.vos
 lib/ocaml/coq/theories/Wellfounded/Union.glob
 lib/ocaml/coq/theories/Wellfounded/Union.v
 lib/ocaml/coq/theories/Wellfounded/Union.vo
+lib/ocaml/coq/theories/Wellfounded/Union.vos
 lib/ocaml/coq/theories/Wellfounded/Well_Ordering.glob
 lib/ocaml/coq/theories/Wellfounded/Well_Ordering.v
 lib/ocaml/coq/theories/Wellfounded/Well_Ordering.vo
+lib/ocaml/coq/theories/Wellfounded/Well_Ordering.vos
 lib/ocaml/coq/theories/Wellfounded/Wellfounded.glob
 lib/ocaml/coq/theories/Wellfounded/Wellfounded.v
 lib/ocaml/coq/theories/Wellfounded/Wellfounded.vo
+lib/ocaml/coq/theories/Wellfounded/Wellfounded.vos
 lib/ocaml/coq/theories/ZArith/
 lib/ocaml/coq/theories/ZArith/.coq-native/
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_BinInt.cmi
@@ -2456,7 +3068,6 @@
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmi
-lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmi
@@ -2469,108 +3080,132 @@
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmi
-lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmi
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmi
 lib/ocaml/coq/theories/ZArith/BinInt.glob
 lib/ocaml/coq/theories/ZArith/BinInt.v
 lib/ocaml/coq/theories/ZArith/BinInt.vo
+lib/ocaml/coq/theories/ZArith/BinInt.vos
 lib/ocaml/coq/theories/ZArith/BinIntDef.glob
 lib/ocaml/coq/theories/ZArith/BinIntDef.v
 lib/ocaml/coq/theories/ZArith/BinIntDef.vo
+lib/ocaml/coq/theories/ZArith/BinIntDef.vos
 lib/ocaml/coq/theories/ZArith/Int.glob
 lib/ocaml/coq/theories/ZArith/Int.v
 lib/ocaml/coq/theories/ZArith/Int.vo
+lib/ocaml/coq/theories/ZArith/Int.vos
 lib/ocaml/coq/theories/ZArith/Wf_Z.glob
 lib/ocaml/coq/theories/ZArith/Wf_Z.v
 lib/ocaml/coq/theories/ZArith/Wf_Z.vo
+lib/ocaml/coq/theories/ZArith/Wf_Z.vos
 lib/ocaml/coq/theories/ZArith/ZArith.glob
 lib/ocaml/coq/theories/ZArith/ZArith.v
 lib/ocaml/coq/theories/ZArith/ZArith.vo
+lib/ocaml/coq/theories/ZArith/ZArith.vos
 lib/ocaml/coq/theories/ZArith/ZArith_base.glob
 lib/ocaml/coq/theories/ZArith/ZArith_base.v
 lib/ocaml/coq/theories/ZArith/ZArith_base.vo
+lib/ocaml/coq/theories/ZArith/ZArith_base.vos
 lib/ocaml/coq/theories/ZArith/ZArith_dec.glob
 lib/ocaml/coq/theories/ZArith/ZArith_dec.v
 lib/ocaml/coq/theories/ZArith/ZArith_dec.vo
+lib/ocaml/coq/theories/ZArith/ZArith_dec.vos
 lib/ocaml/coq/theories/ZArith/Zabs.glob
 lib/ocaml/coq/theories/ZArith/Zabs.v
 lib/ocaml/coq/theories/ZArith/Zabs.vo
+lib/ocaml/coq/theories/ZArith/Zabs.vos
 lib/ocaml/coq/theories/ZArith/Zbool.glob
 lib/ocaml/coq/theories/ZArith/Zbool.v
 lib/ocaml/coq/theories/ZArith/Zbool.vo
+lib/ocaml/coq/theories/ZArith/Zbool.vos
 lib/ocaml/coq/theories/ZArith/Zcompare.glob
 lib/ocaml/coq/theories/ZArith/Zcompare.v
 lib/ocaml/coq/theories/ZArith/Zcompare.vo
+lib/ocaml/coq/theories/ZArith/Zcompare.vos
 lib/ocaml/coq/theories/ZArith/Zcomplements.glob
 lib/ocaml/coq/theories/ZArith/Zcomplements.v
 lib/ocaml/coq/theories/ZArith/Zcomplements.vo
+lib/ocaml/coq/theories/ZArith/Zcomplements.vos
 lib/ocaml/coq/theories/ZArith/Zdigits.glob
 lib/ocaml/coq/theories/ZArith/Zdigits.v
 lib/ocaml/coq/theories/ZArith/Zdigits.vo
+lib/ocaml/coq/theories/ZArith/Zdigits.vos
 lib/ocaml/coq/theories/ZArith/Zdiv.glob
 lib/ocaml/coq/theories/ZArith/Zdiv.v
 lib/ocaml/coq/theories/ZArith/Zdiv.vo
+lib/ocaml/coq/theories/ZArith/Zdiv.vos
 lib/ocaml/coq/theories/ZArith/Zeuclid.glob
 lib/ocaml/coq/theories/ZArith/Zeuclid.v
 lib/ocaml/coq/theories/ZArith/Zeuclid.vo
+lib/ocaml/coq/theories/ZArith/Zeuclid.vos
 lib/ocaml/coq/theories/ZArith/Zeven.glob
 lib/ocaml/coq/theories/ZArith/Zeven.v
 lib/ocaml/coq/theories/ZArith/Zeven.vo
+lib/ocaml/coq/theories/ZArith/Zeven.vos
 lib/ocaml/coq/theories/ZArith/Zgcd_alt.glob
 lib/ocaml/coq/theories/ZArith/Zgcd_alt.v
 lib/ocaml/coq/theories/ZArith/Zgcd_alt.vo
+lib/ocaml/coq/theories/ZArith/Zgcd_alt.vos
 lib/ocaml/coq/theories/ZArith/Zhints.glob
 lib/ocaml/coq/theories/ZArith/Zhints.v
 lib/ocaml/coq/theories/ZArith/Zhints.vo
-lib/ocaml/coq/theories/ZArith/Zlogarithm.glob
-lib/ocaml/coq/theories/ZArith/Zlogarithm.v
-lib/ocaml/coq/theories/ZArith/Zlogarithm.vo
+lib/ocaml/coq/theories/ZArith/Zhints.vos
 lib/ocaml/coq/theories/ZArith/Zmax.glob
 lib/ocaml/coq/theories/ZArith/Zmax.v
 lib/ocaml/coq/theories/ZArith/Zmax.vo
+lib/ocaml/coq/theories/ZArith/Zmax.vos
 lib/ocaml/coq/theories/ZArith/Zmin.glob
 lib/ocaml/coq/theories/ZArith/Zmin.v
 lib/ocaml/coq/theories/ZArith/Zmin.vo
+lib/ocaml/coq/theories/ZArith/Zmin.vos
 lib/ocaml/coq/theories/ZArith/Zminmax.glob
 lib/ocaml/coq/theories/ZArith/Zminmax.v
 lib/ocaml/coq/theories/ZArith/Zminmax.vo
+lib/ocaml/coq/theories/ZArith/Zminmax.vos
 lib/ocaml/coq/theories/ZArith/Zmisc.glob
 lib/ocaml/coq/theories/ZArith/Zmisc.v
 lib/ocaml/coq/theories/ZArith/Zmisc.vo
+lib/ocaml/coq/theories/ZArith/Zmisc.vos
 lib/ocaml/coq/theories/ZArith/Znat.glob
 lib/ocaml/coq/theories/ZArith/Znat.v
 lib/ocaml/coq/theories/ZArith/Znat.vo
+lib/ocaml/coq/theories/ZArith/Znat.vos
 lib/ocaml/coq/theories/ZArith/Znumtheory.glob
 lib/ocaml/coq/theories/ZArith/Znumtheory.v
 lib/ocaml/coq/theories/ZArith/Znumtheory.vo
+lib/ocaml/coq/theories/ZArith/Znumtheory.vos
 lib/ocaml/coq/theories/ZArith/Zorder.glob
 lib/ocaml/coq/theories/ZArith/Zorder.v
 lib/ocaml/coq/theories/ZArith/Zorder.vo
+lib/ocaml/coq/theories/ZArith/Zorder.vos
 lib/ocaml/coq/theories/ZArith/Zpow_alt.glob
 lib/ocaml/coq/theories/ZArith/Zpow_alt.v
 lib/ocaml/coq/theories/ZArith/Zpow_alt.vo
+lib/ocaml/coq/theories/ZArith/Zpow_alt.vos
 lib/ocaml/coq/theories/ZArith/Zpow_def.glob
 lib/ocaml/coq/theories/ZArith/Zpow_def.v
 lib/ocaml/coq/theories/ZArith/Zpow_def.vo
+lib/ocaml/coq/theories/ZArith/Zpow_def.vos
 lib/ocaml/coq/theories/ZArith/Zpow_facts.glob
 lib/ocaml/coq/theories/ZArith/Zpow_facts.v
 lib/ocaml/coq/theories/ZArith/Zpow_facts.vo
+lib/ocaml/coq/theories/ZArith/Zpow_facts.vos
 lib/ocaml/coq/theories/ZArith/Zpower.glob
 lib/ocaml/coq/theories/ZArith/Zpower.v
 lib/ocaml/coq/theories/ZArith/Zpower.vo
+lib/ocaml/coq/theories/ZArith/Zpower.vos
 lib/ocaml/coq/theories/ZArith/Zquot.glob
 lib/ocaml/coq/theories/ZArith/Zquot.v
 lib/ocaml/coq/theories/ZArith/Zquot.vo
-lib/ocaml/coq/theories/ZArith/Zsqrt_compat.glob
-lib/ocaml/coq/theories/ZArith/Zsqrt_compat.v
-lib/ocaml/coq/theories/ZArith/Zsqrt_compat.vo
+lib/ocaml/coq/theories/ZArith/Zquot.vos
 lib/ocaml/coq/theories/ZArith/Zwf.glob
 lib/ocaml/coq/theories/ZArith/Zwf.v
 lib/ocaml/coq/theories/ZArith/Zwf.vo
+lib/ocaml/coq/theories/ZArith/Zwf.vos
 lib/ocaml/coq/theories/ZArith/auxiliary.glob
 lib/ocaml/coq/theories/ZArith/auxiliary.v
 lib/ocaml/coq/theories/ZArith/auxiliary.vo
+lib/ocaml/coq/theories/ZArith/auxiliary.vos
 lib/ocaml/coq/tools/
 lib/ocaml/coq/tools/CoqMakefile.in
 lib/ocaml/coq/tools/TimeFileMaker.py
@@ -2593,39 +3228,144 @@
 lib/ocaml/coq/toplevel/vernac.cmi
 lib/ocaml/coq/toplevel/workerLoop.cmi
 lib/ocaml/coq/user-contrib/
+lib/ocaml/coq/user-contrib/Ltac2/
+lib/ocaml/coq/user-contrib/Ltac2/Array.glob
+lib/ocaml/coq/user-contrib/Ltac2/Array.v
+lib/ocaml/coq/user-contrib/Ltac2/Array.vo
+lib/ocaml/coq/user-contrib/Ltac2/Array.vos
+lib/ocaml/coq/user-contrib/Ltac2/Bool.glob
+lib/ocaml/coq/user-contrib/Ltac2/Bool.v
+lib/ocaml/coq/user-contrib/Ltac2/Bool.vo
+lib/ocaml/coq/user-contrib/Ltac2/Bool.vos
+lib/ocaml/coq/user-contrib/Ltac2/Char.glob
+lib/ocaml/coq/user-contrib/Ltac2/Char.v
+lib/ocaml/coq/user-contrib/Ltac2/Char.vo
+lib/ocaml/coq/user-contrib/Ltac2/Char.vos
+lib/ocaml/coq/user-contrib/Ltac2/Constr.glob
+lib/ocaml/coq/user-contrib/Ltac2/Constr.v
+lib/ocaml/coq/user-contrib/Ltac2/Constr.vo
+lib/ocaml/coq/user-contrib/Ltac2/Constr.vos
+lib/ocaml/coq/user-contrib/Ltac2/Control.glob
+lib/ocaml/coq/user-contrib/Ltac2/Control.v
+lib/ocaml/coq/user-contrib/Ltac2/Control.vo
+lib/ocaml/coq/user-contrib/Ltac2/Control.vos
+lib/ocaml/coq/user-contrib/Ltac2/Env.glob
+lib/ocaml/coq/user-contrib/Ltac2/Env.v
+lib/ocaml/coq/user-contrib/Ltac2/Env.vo
+lib/ocaml/coq/user-contrib/Ltac2/Env.vos
+lib/ocaml/coq/user-contrib/Ltac2/Fresh.glob
+lib/ocaml/coq/user-contrib/Ltac2/Fresh.v
+lib/ocaml/coq/user-contrib/Ltac2/Fresh.vo
+lib/ocaml/coq/user-contrib/Ltac2/Fresh.vos
+lib/ocaml/coq/user-contrib/Ltac2/Ident.glob
+lib/ocaml/coq/user-contrib/Ltac2/Ident.v
+lib/ocaml/coq/user-contrib/Ltac2/Ident.vo
+lib/ocaml/coq/user-contrib/Ltac2/Ident.vos
+lib/ocaml/coq/user-contrib/Ltac2/Init.glob
+lib/ocaml/coq/user-contrib/Ltac2/Init.v
+lib/ocaml/coq/user-contrib/Ltac2/Init.vo
+lib/ocaml/coq/user-contrib/Ltac2/Init.vos
+lib/ocaml/coq/user-contrib/Ltac2/Int.glob
+lib/ocaml/coq/user-contrib/Ltac2/Int.v
+lib/ocaml/coq/user-contrib/Ltac2/Int.vo
+lib/ocaml/coq/user-contrib/Ltac2/Int.vos
+lib/ocaml/coq/user-contrib/Ltac2/List.glob
+lib/ocaml/coq/user-contrib/Ltac2/List.v
+lib/ocaml/coq/user-contrib/Ltac2/List.vo
+lib/ocaml/coq/user-contrib/Ltac2/List.vos
+lib/ocaml/coq/user-contrib/Ltac2/Ltac1.glob
+lib/ocaml/coq/user-contrib/Ltac2/Ltac1.v
+lib/ocaml/coq/user-contrib/Ltac2/Ltac1.vo
+lib/ocaml/coq/user-contrib/Ltac2/Ltac1.vos
+lib/ocaml/coq/user-contrib/Ltac2/Ltac2.glob
+lib/ocaml/coq/user-contrib/Ltac2/Ltac2.v
+lib/ocaml/coq/user-contrib/Ltac2/Ltac2.vo
+lib/ocaml/coq/user-contrib/Ltac2/Ltac2.vos
+lib/ocaml/coq/user-contrib/Ltac2/Message.glob
+lib/ocaml/coq/user-contrib/Ltac2/Message.v
+lib/ocaml/coq/user-contrib/Ltac2/Message.vo
+lib/ocaml/coq/user-contrib/Ltac2/Message.vos
+lib/ocaml/coq/user-contrib/Ltac2/Notations.glob
+lib/ocaml/coq/user-contrib/Ltac2/Notations.v
+lib/ocaml/coq/user-contrib/Ltac2/Notations.vo
+lib/ocaml/coq/user-contrib/Ltac2/Notations.vos
+lib/ocaml/coq/user-contrib/Ltac2/Option.glob
+lib/ocaml/coq/user-contrib/Ltac2/Option.v
+lib/ocaml/coq/user-contrib/Ltac2/Option.vo
+lib/ocaml/coq/user-contrib/Ltac2/Option.vos
+lib/ocaml/coq/user-contrib/Ltac2/Pattern.glob
+lib/ocaml/coq/user-contrib/Ltac2/Pattern.v
+lib/ocaml/coq/user-contrib/Ltac2/Pattern.vo
+lib/ocaml/coq/user-contrib/Ltac2/Pattern.vos
+lib/ocaml/coq/user-contrib/Ltac2/Std.glob
+lib/ocaml/coq/user-contrib/Ltac2/Std.v
+lib/ocaml/coq/user-contrib/Ltac2/Std.vo
+lib/ocaml/coq/user-contrib/Ltac2/Std.vos
+lib/ocaml/coq/user-contrib/Ltac2/String.glob
+lib/ocaml/coq/user-contrib/Ltac2/String.v
+lib/ocaml/coq/user-contrib/Ltac2/String.vo
+lib/ocaml/coq/user-contrib/Ltac2/String.vos
+lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2core.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2dyn.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2entries.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2env.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2expr.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2extffi.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2ffi.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2intern.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2interp.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2match.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2print.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2qexpr.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2quote.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2stdlib.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2tactics.cmi
+lib/ocaml/coq/user-contrib/Ltac2/tac2types.cmi
 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/canonical.cmi
 lib/ocaml/coq/vernac/class.cmi
 lib/ocaml/coq/vernac/classes.cmi
+lib/ocaml/coq/vernac/comArguments.cmi
 lib/ocaml/coq/vernac/comAssumption.cmi
 lib/ocaml/coq/vernac/comDefinition.cmi
 lib/ocaml/coq/vernac/comFixpoint.cmi
 lib/ocaml/coq/vernac/comInductive.cmi
+lib/ocaml/coq/vernac/comPrimitive.cmi
 lib/ocaml/coq/vernac/comProgramFixpoint.cmi
 lib/ocaml/coq/vernac/declareDef.cmi
+lib/ocaml/coq/vernac/declareInd.cmi
+lib/ocaml/coq/vernac/declareObl.cmi
+lib/ocaml/coq/vernac/declareUniv.cmi
+lib/ocaml/coq/vernac/declaremods.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
+lib/ocaml/coq/vernac/library.cmi
+lib/ocaml/coq/vernac/loadpath.cmi
 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/prettyp.cmi
 lib/ocaml/coq/vernac/proof_using.cmi
 lib/ocaml/coq/vernac/pvernac.cmi
+lib/ocaml/coq/vernac/recLemmas.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/vernacexpr.cmi
 lib/ocaml/coq/vernac/vernacextend.cmi
+lib/ocaml/coq/vernac/vernacinterp.cmi
 lib/ocaml/coq/vernac/vernacprop.cmi
 lib/ocaml/coq/vernac/vernacstate.cmi
 @man man/man1/coq-tex.1

Reply | Threaded
Open this post in threaded view
|

Re: [patch] math/coq 8.10.0 -> 8.11.0

Christopher Zimmermann-2

Hi,

the diff including the PLIST changes look correct to me. Nevertheless I
would recommend testing on at least one bytecode-only architecture.
Otherwise this diff is ok with me. Thanks!

Christopher


--
http://gmerlin.de
OpenPGP: http://gmerlin.de/christopher.pub
CB07 DA40 B0B6 571D 35E2  0DEF 87E2 92A7 13E5 DEE1

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: [patch] math/coq 8.10.0 -> 8.11.0

Yozo TODA
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

ok from me too with quick looking diff!

 -- yozo.

-----BEGIN PGP SIGNATURE-----

iQJJBAEBCgAzFiEEsSBE3BD3oI0EPJSvM6KY3A5GNSgFAl5LPLEVHHlvem9AdjAw
Ny52YWlvLm5lLmpwAAoJEDOimNwORjUoIzUP/RshDAqWMxIkwXrs0pzeBxfy4d5m
F1p/c3ysrjKNRRQ/GeLi2NUZDJHh9L/XLyg6BYAb45zd12VINjoN28I+xTfA2XSE
Z0pjwvcgS5/lrLX4m3nMBaPeLRlI/FqQxKiSPnmvqW2wWvFGyvVEbTGkL4qN2dQo
KoeJFGyCmzuhXsYk9IDpWe0nQ2tOf9q/idCYcrs1sYgKEba3HtJYSgHZzIN1x6fI
+UcV2Dn22S/bT/IUpW0X8I9YlLFqMqwXO+q01satIoceZV+V9hnoLGE0Zz7wjdMA
xuo3MAZg7XZXIi90Ew+PnlszlQmUmlml5+kl8G7Pk3+8cDV4OwrKLfPcBz1XiPwk
+k4a7RR/wgeDQ8LDgCCsoXVydAZUkoTbXwJw7G9xQ6Q0aypamk7sjn2LYdgkP2gb
hDkFRWs2+ZsLv3RRSQKChIK4wxu08r022jL4ier9K+JQizGNtvdUvX8+1C2vzpUx
cLt8vuXaBQqZTwPYPMp8cvhAM4jlBRiX1aotd/UOqjE4oHkp7ORqrH5iYyMRk18t
XIr/Pj6yprB5017Zr1DYO2JvJ8bmGSXMNL59HA4btYAIXibbNLqvSgYamc4W+ZbB
O2mwi21vjsk3xLSZRvAnu+C7+BnciV9sVYH5lZjmF6NnWgehJmZDiERvzr641K9B
JhUE0BZM8yLCoR0a
=Gd6G
-----END PGP SIGNATURE-----

Reply | Threaded
Open this post in threaded view
|

Re: [patch] math/coq 8.10.0 -> 8.11.0

Jeremie Courreges-Anglas-2
In reply to this post by Christopher Zimmermann-2
On Mon, Feb 17 2020, Christopher Zimmermann <[hidden email]> wrote:
> Hi,
>
> the diff including the PLIST changes look correct to me. Nevertheless
> I would recommend testing on at least one bytecode-only architecture.

Sadly it doesn't build any more on sparc64.  Error #1 is due to the lack
of -fexcess-precision=standard in base-gcc.

When patching this away or using COMPILER=ports-gcc, I hit error #2:

Error: Error while linking kernel/uint63.cmo:
       The external function `coq_uint63_to_float_byte' is not available

Build log:
  https://pbot.rmdir.de/Y51XNVa7vjKQZb57gOgg0g

--
jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF  DDCC 0DFA 74AE 1524 E7EE

signature.asc (847 bytes) Download Attachment