[diff] math/coq 8.11.2 -> 8.12.0

Here's an updated diff for the latest version of coq.

From the latest aarch64 and powerpc ports bulk builds, it looks like the
version of coq that's in-tree is crashing. Might be worth an update to see
if there's any improvement.

Tested on amd64 with CompCert where everything seems to work.

ok?

Index: Makefile
===================================================================
RCS file: /cvs/ports/math/coq/Makefile,v
retrieving revision 1.50
diff -u -p -u -r1.50 Makefile
--- Makefile 16 Jul 2020 02:50:07 -0000 1.50
+++ Makefile 1 Aug 2020 16:58:37 -0000
@@ -2,7 +2,7 @@

COMMENT= proof assistant based on a typed lambda calculus

-V= 8.11.2
+V= 8.12.0
GH_ACCOUNT = coq
GH_PROJECT = coq
GH_TAGNAME = V${V}
Index: distinfo
===================================================================
RCS file: /cvs/ports/math/coq/distinfo,v
retrieving revision 1.19
diff -u -p -u -r1.19 distinfo
--- distinfo 16 Jul 2020 02:50:07 -0000 1.19
+++ distinfo 1 Aug 2020 16:58:37 -0000
@@ -1,2 +1,2 @@
-SHA256 (coq-8.11.2.tar.gz) = mMueErolCKHKWeDGOPzie/lcNwgrb3zjVXebgLJeG/0=
-SIZE (coq-8.11.2.tar.gz) = 6564523
+SHA256 (coq-8.12.0.tar.gz) = 7N4UxhMvWrtFnn9HJHiHiJKBdK1EhP/4joawCGd5vO4=
+SIZE (coq-8.12.0.tar.gz) = 6774001
Index: pkg/PFRAG.dynlink-native
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PFRAG.dynlink-native,v
retrieving revision 1.7
diff -u -p -u -r1.7 PFRAG.dynlink-native
--- pkg/PFRAG.dynlink-native 1 Jun 2020 06:04:50 -0000 1.7
+++ pkg/PFRAG.dynlink-native 1 Aug 2020 16:58:37 -0000
@@ -1,111 +1,21 @@
@comment $OpenBSD: PFRAG.dynlink-native,v 1.7 2020/06/01 06:04:50 chrisz Exp $
-@bin lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
-@bin lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmxs
-@bin lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmxs
@bin lib/ocaml/coq/plugins/btauto/btauto_plugin.cmxs
@bin lib/ocaml/coq/plugins/cc/cc_plugin.cmxs
-@bin lib/ocaml/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmxs
@bin lib/ocaml/coq/plugins/derive/derive_plugin.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmxs
-@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
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmxs
-@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmxs
@bin lib/ocaml/coq/plugins/extraction/extraction_plugin.cmxs
@bin lib/ocaml/coq/plugins/firstorder/ground_plugin.cmxs
-@bin lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmxs
-@bin lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmxs
@bin lib/ocaml/coq/plugins/funind/recdef_plugin.cmxs
-@bin lib/ocaml/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmxs
@bin lib/ocaml/coq/plugins/ltac/ltac_plugin.cmxs
@bin lib/ocaml/coq/plugins/ltac/tauto_plugin.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RMicromega.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Refl.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RingMicromega.cmxs
-@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Tauto.cmxs
-@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
-@bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaLemmas.cmxs
-@bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaPlugin.cmxs
-@bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaTactic.cmxs
-@bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_PreOmega.cmxs
@bin lib/ocaml/coq/plugins/omega/omega_plugin.cmxs
-@bin lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmxs
-@bin lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmxs
@bin lib/ocaml/coq/plugins/rtauto/rtauto_plugin.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmxs
-@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmxs
-@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/ssrsearch/ssrsearch_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
@@ -135,6 +45,7 @@
@bin lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Wf_nat.cmxs
@bin lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bool.cmxs
@bin lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolEq.cmxs
+@bin lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolOrder.cmxs
@bin lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bvector.cmxs
@bin lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_DecBool.cmxs
@bin lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_IfProp.cmxs
@@ -158,7 +69,7 @@
@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_Coq811.cmxs
-@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmxs
+@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq812.cmxs
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmxs
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmxs
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFullAVL.cmxs
@@ -190,10 +101,13 @@
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmxs
+@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Hexadecimal.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic_Type.cmxs
+@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Ltac.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Nat.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Notations.cmxs
+@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Numeral.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Peano.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Prelude.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmxs
@@ -274,8 +188,16 @@
@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmxs
@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmxs
@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalQ.cmxs
@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmxs
@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalFacts.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalN.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalNat.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalPos.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalQ.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalString.cmxs
+@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalZ.cmxs
@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmxs
@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmxs
@bin lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmxs
@@ -378,13 +300,8 @@
@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_ClassicalConstructiveReals.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
@@ -436,6 +353,7 @@
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_alt.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_calc.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmxs
+@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_facts.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmxs
@@ -444,6 +362,18 @@
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitRmult.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Sqrt_reg.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveAbs.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLUB.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLimits.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveMinMax.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructivePower.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveReals.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.cmxs
+@bin lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveSum.cmxs
+@bin lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.cmxs
+@bin lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyReals.cmxs
+@bin lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.cmxs
+@bin lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveRcomplete.cmxs
@bin lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Operators_Properties.cmxs
@bin lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Definitions.cmxs
@bin lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Operators.cmxs
@@ -471,6 +401,7 @@
@bin lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3.cmxs
@bin lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3_facts.cmxs
@bin lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Uniset.cmxs
+@bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_CPermutation.cmxs
@bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.cmxs
@bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Mergesort.cmxs
@bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_PermutEq.cmxs
@@ -546,4 +477,118 @@
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.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/theories/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
+@bin lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Btauto.cmxs
+@bin lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Reflect.cmxs
+@bin lib/ocaml/coq/theories/derive/.coq-native/NCoq_derive_Derive.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNativeString.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmxs
+@bin lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_Extraction.cmxs
+@bin lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_FunInd.cmxs
+@bin lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_Recdef.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_DeclConstant.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Env.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_EnvRing.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier_util.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lia.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lqa.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lra.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_MExtraction.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_OrderedRing.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Psatz.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_QMicromega.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RMicromega.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Refl.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RingMicromega.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Tauto.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_VarMap.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZArith_hints.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZCoeff.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZMicromega.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Zify.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyBool.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyInst.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyPow.cmxs
+@bin lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Ztac.cmxs
+@bin lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmxs
+@bin lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_NsatzTactic.cmxs
+@bin lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_Omega.cmxs
+@bin lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaLemmas.cmxs
+@bin lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaPlugin.cmxs
+@bin lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaTactic.cmxs
+@bin lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_PreOmega.cmxs
+@bin lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Bintree.cmxs
+@bin lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmxs
+@bin lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmxs
+@bin lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrbool.cmxs
+@bin lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrclasses.cmxs
+@bin lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssreflect.cmxs
+@bin lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrfun.cmxs
+@bin lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmxs
+@bin lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrunder.cmxs
+@bin lib/ocaml/coq/theories/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmxs
+@bin lib/ocaml/coq/theories/ssrsearch/.coq-native/NCoq_ssrsearch_ssrsearch.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmxs
+@bin lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.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.7
diff -u -p -u -r1.7 PFRAG.native
--- pkg/PFRAG.native 1 Jun 2020 06:04:50 -0000 1.7
+++ pkg/PFRAG.native 1 Aug 2020 16:58:38 -0000
@@ -5,7 +5,6 @@
@bin bin/coqqueryworker.opt
@bin bin/coqtacticworker.opt
@bin bin/coqtop.opt
-lib/ocaml/coq/clib/backtrace.cmx
lib/ocaml/coq/clib/bigint.cmx
lib/ocaml/coq/clib/cArray.cmx
lib/ocaml/coq/clib/cEphemeron.cmx
@@ -13,7 +12,6 @@ lib/ocaml/coq/clib/cList.cmx
lib/ocaml/coq/clib/cMap.cmx
lib/ocaml/coq/clib/cObj.cmx
lib/ocaml/coq/clib/cSet.cmx
-lib/ocaml/coq/clib/cStack.cmx
lib/ocaml/coq/clib/cString.cmx
lib/ocaml/coq/clib/cThread.cmx
lib/ocaml/coq/clib/cUnix.cmx
@@ -132,8 +130,8 @@ lib/ocaml/coq/kernel/nativevalues.cmx
lib/ocaml/coq/kernel/opaqueproof.cmx
lib/ocaml/coq/kernel/primred.cmx
lib/ocaml/coq/kernel/reduction.cmx
+lib/ocaml/coq/kernel/relevanceops.cmx
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
@@ -169,6 +167,7 @@ lib/ocaml/coq/lib/hook.cmx
lib/ocaml/coq/lib/lib.a
lib/ocaml/coq/lib/lib.cmxa
lib/ocaml/coq/lib/loc.cmx
+lib/ocaml/coq/lib/objFile.cmx
lib/ocaml/coq/lib/pp.cmx
lib/ocaml/coq/lib/pp_diff.cmx
lib/ocaml/coq/lib/remoteCounter.cmx
@@ -200,12 +199,6 @@ lib/ocaml/coq/parsing/parsing.cmxa
lib/ocaml/coq/parsing/pcoq.cmx
lib/ocaml/coq/parsing/ppextend.cmx
lib/ocaml/coq/parsing/tok.cmx
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmx
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.o
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmx
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.o
lib/ocaml/coq/plugins/btauto/btauto_plugin.cmx
lib/ocaml/coq/plugins/btauto/btauto_plugin.o
lib/ocaml/coq/plugins/btauto/g_btauto.cmx
@@ -216,50 +209,10 @@ lib/ocaml/coq/plugins/cc/ccalgo.cmx
lib/ocaml/coq/plugins/cc/ccproof.cmx
lib/ocaml/coq/plugins/cc/cctac.cmx
lib/ocaml/coq/plugins/cc/g_congruence.cmx
-lib/ocaml/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmx
-lib/ocaml/coq/plugins/derive/.coq-native/NCoq_derive_Derive.o
lib/ocaml/coq/plugins/derive/derive.cmx
lib/ocaml/coq/plugins/derive/derive_plugin.cmx
lib/ocaml/coq/plugins/derive/derive_plugin.o
lib/ocaml/coq/plugins/derive/g_derive.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmx
-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_ExtrOCamlFloats.o
-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
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.o
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmx
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.o
lib/ocaml/coq/plugins/extraction/common.cmx
lib/ocaml/coq/plugins/extraction/extract_env.cmx
lib/ocaml/coq/plugins/extraction/extraction.cmx
@@ -283,10 +236,6 @@ lib/ocaml/coq/plugins/firstorder/instanc
lib/ocaml/coq/plugins/firstorder/rules.cmx
lib/ocaml/coq/plugins/firstorder/sequent.cmx
lib/ocaml/coq/plugins/firstorder/unify.cmx
-lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmx
-lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.o
-lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmx
-lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.o
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
@@ -299,8 +248,6 @@ lib/ocaml/coq/plugins/funind/invfun.cmx
lib/ocaml/coq/plugins/funind/recdef.cmx
lib/ocaml/coq/plugins/funind/recdef_plugin.cmx
lib/ocaml/coq/plugins/funind/recdef_plugin.o
-lib/ocaml/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmx
-lib/ocaml/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.o
lib/ocaml/coq/plugins/ltac/coretactics.cmx
lib/ocaml/coq/plugins/ltac/evar_tactics.cmx
lib/ocaml/coq/plugins/ltac/extraargs.cmx
@@ -312,6 +259,7 @@ lib/ocaml/coq/plugins/ltac/g_ltac.cmx
lib/ocaml/coq/plugins/ltac/g_obligations.cmx
lib/ocaml/coq/plugins/ltac/g_rewrite.cmx
lib/ocaml/coq/plugins/ltac/g_tactic.cmx
+lib/ocaml/coq/plugins/ltac/leminv.cmx
lib/ocaml/coq/plugins/ltac/ltac_plugin.cmx
lib/ocaml/coq/plugins/ltac/ltac_plugin.o
lib/ocaml/coq/plugins/ltac/pltac.cmx
@@ -333,58 +281,6 @@ lib/ocaml/coq/plugins/ltac/tactic_option
lib/ocaml/coq/plugins/ltac/tauto.cmx
lib/ocaml/coq/plugins/ltac/tauto_plugin.cmx
lib/ocaml/coq/plugins/ltac/tauto_plugin.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RMicromega.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RMicromega.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Refl.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Refl.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RingMicromega.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RingMicromega.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Tauto.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Tauto.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmx
-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_Zify.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.o
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.cmx
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.o
lib/ocaml/coq/plugins/micromega/certificate.cmx
lib/ocaml/coq/plugins/micromega/coq_micromega.cmx
lib/ocaml/coq/plugins/micromega/csdpcert.cmx
@@ -396,6 +292,7 @@ lib/ocaml/coq/plugins/micromega/micromeg
lib/ocaml/coq/plugins/micromega/micromega_plugin.cmx
lib/ocaml/coq/plugins/micromega/micromega_plugin.o
lib/ocaml/coq/plugins/micromega/mutils.cmx
+lib/ocaml/coq/plugins/micromega/numCompat.cmx
lib/ocaml/coq/plugins/micromega/persistent_cache.cmx
lib/ocaml/coq/plugins/micromega/polynomial.cmx
lib/ocaml/coq/plugins/micromega/simplex.cmx
@@ -406,8 +303,6 @@ 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/micromega/zify_plugin.o
-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
lib/ocaml/coq/plugins/nsatz/ideal.cmx
lib/ocaml/coq/plugins/nsatz/nsatz.cmx
@@ -415,95 +310,21 @@ lib/ocaml/coq/plugins/nsatz/nsatz_plugin
lib/ocaml/coq/plugins/nsatz/nsatz_plugin.o
lib/ocaml/coq/plugins/nsatz/polynom.cmx
lib/ocaml/coq/plugins/nsatz/utile.cmx
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmx
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.o
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaLemmas.cmx
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaLemmas.o
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaPlugin.cmx
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaPlugin.o
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaTactic.cmx
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaTactic.o
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_PreOmega.cmx
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_PreOmega.o
lib/ocaml/coq/plugins/omega/coq_omega.cmx
lib/ocaml/coq/plugins/omega/g_omega.cmx
lib/ocaml/coq/plugins/omega/omega.cmx
lib/ocaml/coq/plugins/omega/omega_plugin.cmx
lib/ocaml/coq/plugins/omega/omega_plugin.o
-lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx
-lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.o
-lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmx
-lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.o
lib/ocaml/coq/plugins/rtauto/g_rtauto.cmx
lib/ocaml/coq/plugins/rtauto/proof_search.cmx
lib/ocaml/coq/plugins/rtauto/refl_tauto.cmx
lib/ocaml/coq/plugins/rtauto/rtauto_plugin.cmx
lib/ocaml/coq/plugins/rtauto/rtauto_plugin.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.o
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmx
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.o
lib/ocaml/coq/plugins/setoid_ring/g_newring.cmx
lib/ocaml/coq/plugins/setoid_ring/newring.cmx
lib/ocaml/coq/plugins/setoid_ring/newring_ast.cmx
lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmx
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_ssrclasses.o
-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_ssrsetoid.o
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmx
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.o
lib/ocaml/coq/plugins/ssr/ssrbwd.cmx
lib/ocaml/coq/plugins/ssr/ssrcommon.cmx
lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmx
@@ -517,12 +338,13 @@ lib/ocaml/coq/plugins/ssr/ssrprinters.cm
lib/ocaml/coq/plugins/ssr/ssrtacticals.cmx
lib/ocaml/coq/plugins/ssr/ssrvernac.cmx
lib/ocaml/coq/plugins/ssr/ssrview.cmx
-lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmx
-lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.o
lib/ocaml/coq/plugins/ssrmatching/g_ssrmatching.cmx
lib/ocaml/coq/plugins/ssrmatching/ssrmatching.cmx
lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmx
lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.o
+lib/ocaml/coq/plugins/ssrsearch/g_search.cmx
+lib/ocaml/coq/plugins/ssrsearch/ssrsearch_plugin.cmx
+lib/ocaml/coq/plugins/ssrsearch/ssrsearch_plugin.o
lib/ocaml/coq/plugins/syntax/float_syntax.cmx
lib/ocaml/coq/plugins/syntax/float_syntax_plugin.cmx
lib/ocaml/coq/plugins/syntax/float_syntax_plugin.o
@@ -543,8 +365,8 @@ lib/ocaml/coq/plugins/syntax/string_nota
lib/ocaml/coq/pretyping/arguments_renaming.cmx
lib/ocaml/coq/pretyping/cases.cmx
lib/ocaml/coq/pretyping/cbv.cmx
-lib/ocaml/coq/pretyping/classops.cmx
lib/ocaml/coq/pretyping/coercion.cmx
+lib/ocaml/coq/pretyping/coercionops.cmx
lib/ocaml/coq/pretyping/constr_matching.cmx
lib/ocaml/coq/pretyping/detyping.cmx
lib/ocaml/coq/pretyping/evarconv.cmx
@@ -622,8 +444,8 @@ lib/ocaml/coq/tactics/autorewrite.cmx
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/declareUctx.cmx
lib/ocaml/coq/tactics/dn.cmx
lib/ocaml/coq/tactics/dnet.cmx
lib/ocaml/coq/tactics/eauto.cmx
@@ -637,10 +459,7 @@ lib/ocaml/coq/tactics/hints.cmx
lib/ocaml/coq/tactics/hipattern.cmx
lib/ocaml/coq/tactics/ind_tables.cmx
lib/ocaml/coq/tactics/inv.cmx
-lib/ocaml/coq/tactics/leminv.cmx
-lib/ocaml/coq/tactics/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
@@ -696,6 +515,8 @@ lib/ocaml/coq/theories/Bool/.coq-native/
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bool.o
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolEq.cmx
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolEq.o
+lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolOrder.cmx
+lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolOrder.o
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bvector.cmx
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bvector.o
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_DecBool.cmx
@@ -742,8 +563,8 @@ lib/ocaml/coq/theories/Compat/.coq-nativ
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.o
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.cmx
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.o
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmx
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.o
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq812.cmx
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq812.o
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmx
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.o
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmx
@@ -806,14 +627,20 @@ lib/ocaml/coq/theories/Init/.coq-native/
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmx
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.o
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Hexadecimal.cmx
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Hexadecimal.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmx
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic_Type.cmx
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic_Type.o
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Ltac.cmx
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Ltac.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Nat.cmx
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Nat.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Notations.cmx
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Notations.o
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Numeral.cmx
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Numeral.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Peano.cmx
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Peano.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Prelude.cmx
@@ -974,10 +801,26 @@ lib/ocaml/coq/theories/Numbers/.coq-nati
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.o
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmx
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalQ.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalQ.o
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmx
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.o
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmx
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalFacts.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalFacts.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalN.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalN.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalNat.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalNat.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalPos.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalPos.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalQ.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalQ.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalString.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalString.o
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalZ.cmx
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalZ.o
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmx
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.o
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmx
@@ -1182,20 +1025,10 @@ lib/ocaml/coq/theories/Reals/.coq-native
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_ClassicalConstructiveReals.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalConstructiveReals.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.o
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmx
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.o
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmx
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.o
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmx
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.o
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmx
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.o
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmx
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.o
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmx
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.o
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
@@ -1298,6 +1131,8 @@ lib/ocaml/coq/theories/Reals/.coq-native
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_calc.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.o
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_facts.cmx
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_facts.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmx
@@ -1314,6 +1149,30 @@ lib/ocaml/coq/theories/Reals/.coq-native
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitRmult.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Sqrt_reg.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Sqrt_reg.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveAbs.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveAbs.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLUB.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLUB.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLimits.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLimits.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveMinMax.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveMinMax.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructivePower.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructivePower.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveReals.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveReals.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.o
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveSum.cmx
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveSum.o
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.cmx
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.o
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyReals.cmx
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyReals.o
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.cmx
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.o
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveRcomplete.cmx
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveRcomplete.o
lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Operators_Properties.cmx
lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Operators_Properties.o
lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Definitions.cmx
@@ -1368,6 +1227,8 @@ lib/ocaml/coq/theories/Sets/.coq-native/
lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3_facts.o
lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Uniset.cmx
lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Uniset.o
+lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_CPermutation.cmx
+lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_CPermutation.o
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.cmx
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.o
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Mergesort.cmx
@@ -1518,6 +1379,196 @@ lib/ocaml/coq/theories/ZArith/.coq-nativ
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.o
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Algebra.cmx
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Algebra.o
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Btauto.cmx
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Btauto.o
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Reflect.cmx
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Reflect.o
+lib/ocaml/coq/theories/derive/.coq-native/NCoq_derive_Derive.cmx
+lib/ocaml/coq/theories/derive/.coq-native/NCoq_derive_Derive.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNativeString.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNativeString.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.o
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_Extraction.cmx
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_Extraction.o
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_FunInd.cmx
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_FunInd.o
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_Recdef.cmx
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_Recdef.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_DeclConstant.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_DeclConstant.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Env.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Env.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_EnvRing.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_EnvRing.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier_util.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier_util.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lia.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lia.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lqa.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lqa.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lra.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lra.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_MExtraction.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_MExtraction.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_OrderedRing.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_OrderedRing.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Psatz.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Psatz.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_QMicromega.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_QMicromega.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RMicromega.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RMicromega.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Refl.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Refl.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RingMicromega.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RingMicromega.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Tauto.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Tauto.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_VarMap.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_VarMap.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZArith_hints.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZArith_hints.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZCoeff.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZCoeff.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZMicromega.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZMicromega.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Zify.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Zify.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyBool.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyBool.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyClasses.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyComparison.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyInst.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyInst.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyPow.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyPow.o
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Ztac.cmx
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Ztac.o
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmx
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_Nsatz.o
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_NsatzTactic.cmx
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_NsatzTactic.o
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_Omega.cmx
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_Omega.o
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaLemmas.cmx
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaLemmas.o
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaPlugin.cmx
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaPlugin.o
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaTactic.cmx
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaTactic.o
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_PreOmega.cmx
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_PreOmega.o
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Bintree.o
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmx
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Rtauto.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.o
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmx
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.o
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrbool.cmx
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrbool.o
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrclasses.cmx
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrclasses.o
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssreflect.cmx
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssreflect.o
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrfun.cmx
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrfun.o
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmx
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrsetoid.o
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrunder.cmx
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrunder.o
+lib/ocaml/coq/theories/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmx
+lib/ocaml/coq/theories/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.o
+lib/ocaml/coq/theories/ssrsearch/.coq-native/NCoq_ssrsearch_ssrsearch.cmx
+lib/ocaml/coq/theories/ssrsearch/.coq-native/NCoq_ssrsearch_ssrsearch.o
lib/ocaml/coq/topbin/
lib/ocaml/coq/topbin/coqc_bin.cmx
lib/ocaml/coq/topbin/coqproofworker_bin.cmx
@@ -1537,6 +1588,44 @@ lib/ocaml/coq/toplevel/toplevel.cmxa
lib/ocaml/coq/toplevel/usage.cmx
lib/ocaml/coq/toplevel/vernac.cmx
lib/ocaml/coq/toplevel/workerLoop.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.o
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmx
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.o
lib/ocaml/coq/user-contrib/Ltac2/g_ltac2.cmx
lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmx
lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.o
@@ -1557,15 +1646,18 @@ 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/comCoercion.cmx
lib/ocaml/coq/vernac/comDefinition.cmx
lib/ocaml/coq/vernac/comFixpoint.cmx
+lib/ocaml/coq/vernac/comHints.cmx
lib/ocaml/coq/vernac/comInductive.cmx
lib/ocaml/coq/vernac/comPrimitive.cmx
lib/ocaml/coq/vernac/comProgramFixpoint.cmx
+lib/ocaml/coq/vernac/comSearch.cmx
+lib/ocaml/coq/vernac/declare.cmx
lib/ocaml/coq/vernac/declareDef.cmx
lib/ocaml/coq/vernac/declareInd.cmx
lib/ocaml/coq/vernac/declareObl.cmx
@@ -1584,12 +1676,15 @@ 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/pfedit.cmx
lib/ocaml/coq/vernac/ppvernac.cmx
lib/ocaml/coq/vernac/prettyp.cmx
+lib/ocaml/coq/vernac/proof_global.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/retrieveObl.cmx
lib/ocaml/coq/vernac/search.cmx
lib/ocaml/coq/vernac/topfmt.cmx
lib/ocaml/coq/vernac/vernac.a
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PLIST,v
retrieving revision 1.15
diff -u -p -u -r1.15 PLIST
--- pkg/PLIST 1 Jun 2020 06:04:50 -0000 1.15
+++ pkg/PLIST 1 Aug 2020 16:58:38 -0000
@@ -18,11 +18,11 @@ bin/coqpp
@comment bin/coqtop.byte
@bin bin/coqwc
@bin bin/coqworkmgr
+@bin bin/ocamllibdep
@bin bin/votour
lib/ocaml/coq/
lib/ocaml/coq/META
lib/ocaml/coq/clib/
-lib/ocaml/coq/clib/backtrace.cmi
lib/ocaml/coq/clib/bigint.cmi
lib/ocaml/coq/clib/cArray.cmi
lib/ocaml/coq/clib/cEphemeron.cmi
@@ -31,7 +31,6 @@ lib/ocaml/coq/clib/cMap.cmi
lib/ocaml/coq/clib/cObj.cmi
lib/ocaml/coq/clib/cSet.cmi
lib/ocaml/coq/clib/cSig.cmi
-lib/ocaml/coq/clib/cStack.cmi
lib/ocaml/coq/clib/cString.cmi
lib/ocaml/coq/clib/cThread.cmi
lib/ocaml/coq/clib/cUnix.cmi
@@ -184,8 +183,8 @@ lib/ocaml/coq/kernel/nativevalues.cmi
lib/ocaml/coq/kernel/opaqueproof.cmi
lib/ocaml/coq/kernel/primred.cmi
lib/ocaml/coq/kernel/reduction.cmi
+lib/ocaml/coq/kernel/relevanceops.cmi
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
@@ -220,6 +219,7 @@ lib/ocaml/coq/lib/future.cmi
lib/ocaml/coq/lib/genarg.cmi
lib/ocaml/coq/lib/hook.cmi
lib/ocaml/coq/lib/loc.cmi
+lib/ocaml/coq/lib/objFile.cmi
lib/ocaml/coq/lib/pp.cmi
lib/ocaml/coq/lib/pp_diff.cmi
lib/ocaml/coq/lib/remoteCounter.cmi
@@ -252,22 +252,6 @@ lib/ocaml/coq/parsing/ppextend.cmi
lib/ocaml/coq/parsing/tok.cmi
lib/ocaml/coq/plugins/
lib/ocaml/coq/plugins/btauto/
-lib/ocaml/coq/plugins/btauto/.coq-native/
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmi
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmi
-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/
@@ -276,111 +260,9 @@ lib/ocaml/coq/plugins/cc/ccalgo.cmi
lib/ocaml/coq/plugins/cc/ccproof.cmi
lib/ocaml/coq/plugins/cc/cctac.cmi
lib/ocaml/coq/plugins/derive/
-lib/ocaml/coq/plugins/derive/.coq-native/
-lib/ocaml/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
-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/
-lib/ocaml/coq/plugins/extraction/.coq-native/
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmi
-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
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmi
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmi
-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
@@ -402,17 +284,6 @@ lib/ocaml/coq/plugins/firstorder/rules.c
lib/ocaml/coq/plugins/firstorder/sequent.cmi
lib/ocaml/coq/plugins/firstorder/unify.cmi
lib/ocaml/coq/plugins/funind/
-lib/ocaml/coq/plugins/funind/.coq-native/
-lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmi
-lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmi
-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
@@ -424,15 +295,10 @@ lib/ocaml/coq/plugins/funind/invfun.cmi
lib/ocaml/coq/plugins/funind/recdef.cmi
lib/ocaml/coq/plugins/funind/recdef_plugin.cmi
lib/ocaml/coq/plugins/ltac/
-lib/ocaml/coq/plugins/ltac/.coq-native/
-lib/ocaml/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmi
-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
+lib/ocaml/coq/plugins/ltac/leminv.cmi
lib/ocaml/coq/plugins/ltac/ltac_plugin.cmi
lib/ocaml/coq/plugins/ltac/pltac.cmi
lib/ocaml/coq/plugins/ltac/pptactic.cmi
@@ -452,137 +318,6 @@ lib/ocaml/coq/plugins/ltac/tactic_option
lib/ocaml/coq/plugins/ltac/tauto.cmi
lib/ocaml/coq/plugins/ltac/tauto_plugin.cmi
lib/ocaml/coq/plugins/micromega/
-lib/ocaml/coq/plugins/micromega/.coq-native/
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RMicromega.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Refl.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RingMicromega.cmi
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Tauto.cmi
-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
@@ -593,6 +328,7 @@ lib/ocaml/coq/plugins/micromega/mfourier
lib/ocaml/coq/plugins/micromega/micromega.cmi
lib/ocaml/coq/plugins/micromega/micromega_plugin.cmi
lib/ocaml/coq/plugins/micromega/mutils.cmi
+lib/ocaml/coq/plugins/micromega/numCompat.cmi
lib/ocaml/coq/plugins/micromega/persistent_cache.cmi
lib/ocaml/coq/plugins/micromega/polynomial.cmi
lib/ocaml/coq/plugins/micromega/simplex.cmi
@@ -603,241 +339,42 @@ 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
lib/ocaml/coq/plugins/nsatz/polynom.cmi
lib/ocaml/coq/plugins/nsatz/utile.cmi
lib/ocaml/coq/plugins/omega/
-lib/ocaml/coq/plugins/omega/.coq-native/
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmi
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaLemmas.cmi
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaPlugin.cmi
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaTactic.cmi
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_PreOmega.cmi
-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/
-lib/ocaml/coq/plugins/rtauto/.coq-native/
-lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
-lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmi
-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
lib/ocaml/coq/plugins/setoid_ring/
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmi
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmi
-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/
-lib/ocaml/coq/plugins/ssrmatching/.coq-native/
-lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
lib/ocaml/coq/plugins/ssrmatching/g_ssrmatching.cmi
lib/ocaml/coq/plugins/ssrmatching/ssrmatching.cmi
-lib/ocaml/coq/plugins/ssrmatching/ssrmatching.glob
-lib/ocaml/coq/plugins/ssrmatching/ssrmatching.v
-lib/ocaml/coq/plugins/ssrmatching/ssrmatching.vo
-lib/ocaml/coq/plugins/ssrmatching/ssrmatching.vos
lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
+lib/ocaml/coq/plugins/ssrsearch/
+lib/ocaml/coq/plugins/ssrsearch/ssrsearch_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
@@ -851,8 +388,8 @@ lib/ocaml/coq/pretyping/
lib/ocaml/coq/pretyping/arguments_renaming.cmi
lib/ocaml/coq/pretyping/cases.cmi
lib/ocaml/coq/pretyping/cbv.cmi
-lib/ocaml/coq/pretyping/classops.cmi
lib/ocaml/coq/pretyping/coercion.cmi
+lib/ocaml/coq/pretyping/coercionops.cmi
lib/ocaml/coq/pretyping/constr_matching.cmi
lib/ocaml/coq/pretyping/detyping.cmi
lib/ocaml/coq/pretyping/evarconv.cmi
@@ -925,8 +462,8 @@ lib/ocaml/coq/tactics/autorewrite.cmi
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/declareUctx.cmi
lib/ocaml/coq/tactics/dn.cmi
lib/ocaml/coq/tactics/dnet.cmi
lib/ocaml/coq/tactics/eauto.cmi
@@ -940,10 +477,7 @@ lib/ocaml/coq/tactics/hints.cmi
lib/ocaml/coq/tactics/hipattern.cmi
lib/ocaml/coq/tactics/ind_tables.cmi
lib/ocaml/coq/tactics/inv.cmi
-lib/ocaml/coq/tactics/leminv.cmi
-lib/ocaml/coq/tactics/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
@@ -1066,6 +600,7 @@ lib/ocaml/coq/theories/Bool/
lib/ocaml/coq/theories/Bool/.coq-native/
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bool.cmi
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolEq.cmi
+lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolOrder.cmi
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bvector.cmi
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_DecBool.cmi
lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_IfProp.cmi
@@ -1079,6 +614,10 @@ 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/BoolOrder.glob
+lib/ocaml/coq/theories/Bool/BoolOrder.v
+lib/ocaml/coq/theories/Bool/BoolOrder.vo
+lib/ocaml/coq/theories/Bool/BoolOrder.vos
lib/ocaml/coq/theories/Bool/Bvector.glob
lib/ocaml/coq/theories/Bool/Bvector.v
lib/ocaml/coq/theories/Bool/Bvector.vo
@@ -1181,7 +720,7 @@ lib/ocaml/coq/theories/Compat/.coq-nativ
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_Coq811.cmi
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmi
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq812.cmi
lib/ocaml/coq/theories/Compat/AdmitAxiom.glob
lib/ocaml/coq/theories/Compat/AdmitAxiom.v
lib/ocaml/coq/theories/Compat/AdmitAxiom.vo
@@ -1194,10 +733,10 @@ lib/ocaml/coq/theories/Compat/Coq811.glo
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/Compat/Coq812.glob
+lib/ocaml/coq/theories/Compat/Coq812.v
+lib/ocaml/coq/theories/Compat/Coq812.vo
+lib/ocaml/coq/theories/Compat/Coq812.vos
lib/ocaml/coq/theories/FSets/
lib/ocaml/coq/theories/FSets/.coq-native/
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
@@ -1347,10 +886,13 @@ lib/ocaml/coq/theories/Init/.coq-native/
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmi
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Hexadecimal.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic_Type.cmi
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Ltac.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Nat.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Notations.cmi
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Numeral.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Peano.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Prelude.cmi
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmi
@@ -1369,6 +911,10 @@ 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/Hexadecimal.glob
+lib/ocaml/coq/theories/Init/Hexadecimal.v
+lib/ocaml/coq/theories/Init/Hexadecimal.vo
+lib/ocaml/coq/theories/Init/Hexadecimal.vos
lib/ocaml/coq/theories/Init/Logic.glob
lib/ocaml/coq/theories/Init/Logic.v
lib/ocaml/coq/theories/Init/Logic.vo
@@ -1377,6 +923,10 @@ lib/ocaml/coq/theories/Init/Logic_Type.g
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/Ltac.glob
+lib/ocaml/coq/theories/Init/Ltac.v
+lib/ocaml/coq/theories/Init/Ltac.vo
+lib/ocaml/coq/theories/Init/Ltac.vos
lib/ocaml/coq/theories/Init/Nat.glob
lib/ocaml/coq/theories/Init/Nat.v
lib/ocaml/coq/theories/Init/Nat.vo
@@ -1385,6 +935,10 @@ lib/ocaml/coq/theories/Init/Notations.gl
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/Numeral.glob
+lib/ocaml/coq/theories/Init/Numeral.v
+lib/ocaml/coq/theories/Init/Numeral.vo
+lib/ocaml/coq/theories/Init/Numeral.vos
lib/ocaml/coq/theories/Init/Peano.glob
lib/ocaml/coq/theories/Init/Peano.v
lib/ocaml/coq/theories/Init/Peano.vo
@@ -1765,8 +1319,16 @@ lib/ocaml/coq/theories/Numbers/.coq-nati
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmi
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmi
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalQ.cmi
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmi
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalFacts.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalN.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalNat.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalPos.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalQ.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalString.cmi
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalZ.cmi
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmi
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmi
lib/ocaml/coq/theories/Numbers/AltBinNotations.glob
@@ -1852,6 +1414,10 @@ lib/ocaml/coq/theories/Numbers/DecimalPo
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/DecimalQ.glob
+lib/ocaml/coq/theories/Numbers/DecimalQ.v
+lib/ocaml/coq/theories/Numbers/DecimalQ.vo
+lib/ocaml/coq/theories/Numbers/DecimalQ.vos
lib/ocaml/coq/theories/Numbers/DecimalString.glob
lib/ocaml/coq/theories/Numbers/DecimalString.v
lib/ocaml/coq/theories/Numbers/DecimalString.vo
@@ -1860,6 +1426,34 @@ lib/ocaml/coq/theories/Numbers/DecimalZ.
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/HexadecimalFacts.glob
+lib/ocaml/coq/theories/Numbers/HexadecimalFacts.v
+lib/ocaml/coq/theories/Numbers/HexadecimalFacts.vo
+lib/ocaml/coq/theories/Numbers/HexadecimalFacts.vos
+lib/ocaml/coq/theories/Numbers/HexadecimalN.glob
+lib/ocaml/coq/theories/Numbers/HexadecimalN.v
+lib/ocaml/coq/theories/Numbers/HexadecimalN.vo
+lib/ocaml/coq/theories/Numbers/HexadecimalN.vos
+lib/ocaml/coq/theories/Numbers/HexadecimalNat.glob
+lib/ocaml/coq/theories/Numbers/HexadecimalNat.v
+lib/ocaml/coq/theories/Numbers/HexadecimalNat.vo
+lib/ocaml/coq/theories/Numbers/HexadecimalNat.vos
+lib/ocaml/coq/theories/Numbers/HexadecimalPos.glob
+lib/ocaml/coq/theories/Numbers/HexadecimalPos.v
+lib/ocaml/coq/theories/Numbers/HexadecimalPos.vo
+lib/ocaml/coq/theories/Numbers/HexadecimalPos.vos
+lib/ocaml/coq/theories/Numbers/HexadecimalQ.glob
+lib/ocaml/coq/theories/Numbers/HexadecimalQ.v
+lib/ocaml/coq/theories/Numbers/HexadecimalQ.vo
+lib/ocaml/coq/theories/Numbers/HexadecimalQ.vos
+lib/ocaml/coq/theories/Numbers/HexadecimalString.glob
+lib/ocaml/coq/theories/Numbers/HexadecimalString.v
+lib/ocaml/coq/theories/Numbers/HexadecimalString.vo
+lib/ocaml/coq/theories/Numbers/HexadecimalString.vos
+lib/ocaml/coq/theories/Numbers/HexadecimalZ.glob
+lib/ocaml/coq/theories/Numbers/HexadecimalZ.v
+lib/ocaml/coq/theories/Numbers/HexadecimalZ.vo
+lib/ocaml/coq/theories/Numbers/HexadecimalZ.vos
lib/ocaml/coq/theories/Numbers/Integer/
lib/ocaml/coq/theories/Numbers/Integer/Abstract/
lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/
@@ -2322,13 +1916,8 @@ lib/ocaml/coq/theories/Reals/.coq-native
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_ClassicalConstructiveReals.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
@@ -2380,6 +1969,7 @@ lib/ocaml/coq/theories/Reals/.coq-native
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_alt.cmi
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_calc.cmi
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmi
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_facts.cmi
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmi
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmi
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmi
@@ -2388,6 +1978,48 @@ lib/ocaml/coq/theories/Reals/.coq-native
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmi
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitRmult.cmi
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Sqrt_reg.cmi
+lib/ocaml/coq/theories/Reals/Abstract/
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveAbs.cmi
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLUB.cmi
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLimits.cmi
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveMinMax.cmi
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructivePower.cmi
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveReals.cmi
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.cmi
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveSum.cmi
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveAbs.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveAbs.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveAbs.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveAbs.vos
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLUB.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLUB.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLUB.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLUB.vos
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLimits.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLimits.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLimits.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveLimits.vos
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveMinMax.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveMinMax.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveMinMax.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveMinMax.vos
+lib/ocaml/coq/theories/Reals/Abstract/ConstructivePower.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructivePower.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructivePower.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructivePower.vos
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveReals.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveReals.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveReals.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveReals.vos
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveRealsMorphisms.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveRealsMorphisms.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveRealsMorphisms.vos
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveSum.glob
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveSum.v
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveSum.vo
+lib/ocaml/coq/theories/Reals/Abstract/ConstructiveSum.vos
lib/ocaml/coq/theories/Reals/Alembert.glob
lib/ocaml/coq/theories/Reals/Alembert.v
lib/ocaml/coq/theories/Reals/Alembert.vo
@@ -2404,38 +2036,40 @@ lib/ocaml/coq/theories/Reals/Binomial.gl
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/
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.cmi
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyReals.cmi
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.cmi
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveRcomplete.cmi
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyAbs.glob
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyAbs.v
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyAbs.vo
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyAbs.vos
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyReals.glob
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyReals.v
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyReals.vo
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyReals.vos
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.glob
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.vo
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.vos
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveRcomplete.glob
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveRcomplete.v
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveRcomplete.vo
+lib/ocaml/coq/theories/Reals/Cauchy/ConstructiveRcomplete.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/ClassicalConstructiveReals.glob
+lib/ocaml/coq/theories/Reals/ClassicalConstructiveReals.v
+lib/ocaml/coq/theories/Reals/ClassicalConstructiveReals.vo
+lib/ocaml/coq/theories/Reals/ClassicalConstructiveReals.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
@@ -2640,6 +2274,10 @@ lib/ocaml/coq/theories/Reals/Rtrigo_def.
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_facts.glob
+lib/ocaml/coq/theories/Reals/Rtrigo_facts.v
+lib/ocaml/coq/theories/Reals/Rtrigo_facts.vo
+lib/ocaml/coq/theories/Reals/Rtrigo_facts.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
@@ -2815,6 +2453,7 @@ 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_CPermutation.cmi
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.cmi
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Mergesort.cmi
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_PermutEq.cmi
@@ -2822,6 +2461,10 @@ lib/ocaml/coq/theories/Sorting/.coq-nati
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Permutation.cmi
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorted.cmi
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorting.cmi
+lib/ocaml/coq/theories/Sorting/CPermutation.glob
+lib/ocaml/coq/theories/Sorting/CPermutation.v
+lib/ocaml/coq/theories/Sorting/CPermutation.vo
+lib/ocaml/coq/theories/Sorting/CPermutation.vos
lib/ocaml/coq/theories/Sorting/Heap.glob
lib/ocaml/coq/theories/Sorting/Heap.v
lib/ocaml/coq/theories/Sorting/Heap.vo
@@ -3202,6 +2845,505 @@ lib/ocaml/coq/theories/ZArith/auxiliary.
lib/ocaml/coq/theories/ZArith/auxiliary.v
lib/ocaml/coq/theories/ZArith/auxiliary.vo
lib/ocaml/coq/theories/ZArith/auxiliary.vos
+lib/ocaml/coq/theories/btauto/
+lib/ocaml/coq/theories/btauto/.coq-native/
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Algebra.cmi
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Btauto.cmi
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Reflect.cmi
+lib/ocaml/coq/theories/btauto/Algebra.glob
+lib/ocaml/coq/theories/btauto/Algebra.v
+lib/ocaml/coq/theories/btauto/Algebra.vo
+lib/ocaml/coq/theories/btauto/Algebra.vos
+lib/ocaml/coq/theories/btauto/Btauto.glob
+lib/ocaml/coq/theories/btauto/Btauto.v
+lib/ocaml/coq/theories/btauto/Btauto.vo
+lib/ocaml/coq/theories/btauto/Btauto.vos
+lib/ocaml/coq/theories/btauto/Reflect.glob
+lib/ocaml/coq/theories/btauto/Reflect.v
+lib/ocaml/coq/theories/btauto/Reflect.vo
+lib/ocaml/coq/theories/btauto/Reflect.vos
+lib/ocaml/coq/theories/derive/
+lib/ocaml/coq/theories/derive/.coq-native/
+lib/ocaml/coq/theories/derive/.coq-native/NCoq_derive_Derive.cmi
+lib/ocaml/coq/theories/derive/Derive.glob
+lib/ocaml/coq/theories/derive/Derive.v
+lib/ocaml/coq/theories/derive/Derive.vo
+lib/ocaml/coq/theories/derive/Derive.vos
+lib/ocaml/coq/theories/extraction/
+lib/ocaml/coq/theories/extraction/.coq-native/
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNativeString.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmi
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_Extraction.cmi
+lib/ocaml/coq/theories/extraction/ExtrHaskellBasic.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellBasic.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellBasic.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellBasic.vos
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInt.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInt.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInt.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInt.vos
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInteger.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInteger.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInteger.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatInteger.vos
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatNum.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatNum.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatNum.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellNatNum.vos
+lib/ocaml/coq/theories/extraction/ExtrHaskellString.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellString.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellString.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellString.vos
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInt.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInt.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInt.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInt.vos
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInteger.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInteger.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInteger.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellZInteger.vos
+lib/ocaml/coq/theories/extraction/ExtrHaskellZNum.glob
+lib/ocaml/coq/theories/extraction/ExtrHaskellZNum.v
+lib/ocaml/coq/theories/extraction/ExtrHaskellZNum.vo
+lib/ocaml/coq/theories/extraction/ExtrHaskellZNum.vos
+lib/ocaml/coq/theories/extraction/ExtrOCamlFloats.glob
+lib/ocaml/coq/theories/extraction/ExtrOCamlFloats.v
+lib/ocaml/coq/theories/extraction/ExtrOCamlFloats.vo
+lib/ocaml/coq/theories/extraction/ExtrOCamlFloats.vos
+lib/ocaml/coq/theories/extraction/ExtrOCamlInt63.glob
+lib/ocaml/coq/theories/extraction/ExtrOCamlInt63.v
+lib/ocaml/coq/theories/extraction/ExtrOCamlInt63.vo
+lib/ocaml/coq/theories/extraction/ExtrOCamlInt63.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlBasic.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlBasic.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlBasic.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlBasic.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlBigIntConv.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlBigIntConv.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlBigIntConv.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlBigIntConv.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlChar.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlChar.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlChar.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlChar.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlIntConv.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlIntConv.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlIntConv.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlIntConv.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatBigInt.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatBigInt.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatBigInt.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatBigInt.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatInt.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatInt.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatInt.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlNatInt.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlNativeString.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlNativeString.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlNativeString.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlNativeString.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlString.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlString.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlString.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlString.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlZBigInt.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlZBigInt.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlZBigInt.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlZBigInt.vos
+lib/ocaml/coq/theories/extraction/ExtrOcamlZInt.glob
+lib/ocaml/coq/theories/extraction/ExtrOcamlZInt.v
+lib/ocaml/coq/theories/extraction/ExtrOcamlZInt.vo
+lib/ocaml/coq/theories/extraction/ExtrOcamlZInt.vos
+lib/ocaml/coq/theories/extraction/Extraction.glob
+lib/ocaml/coq/theories/extraction/Extraction.v
+lib/ocaml/coq/theories/extraction/Extraction.vo
+lib/ocaml/coq/theories/extraction/Extraction.vos
+lib/ocaml/coq/theories/funind/
+lib/ocaml/coq/theories/funind/.coq-native/
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_FunInd.cmi
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_Recdef.cmi
+lib/ocaml/coq/theories/funind/FunInd.glob
+lib/ocaml/coq/theories/funind/FunInd.v
+lib/ocaml/coq/theories/funind/FunInd.vo
+lib/ocaml/coq/theories/funind/FunInd.vos
+lib/ocaml/coq/theories/funind/Recdef.glob
+lib/ocaml/coq/theories/funind/Recdef.v
+lib/ocaml/coq/theories/funind/Recdef.vo
+lib/ocaml/coq/theories/funind/Recdef.vos
+lib/ocaml/coq/theories/micromega/
+lib/ocaml/coq/theories/micromega/.coq-native/
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_DeclConstant.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Env.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier_util.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lia.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lqa.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lra.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_MExtraction.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Psatz.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_QMicromega.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RMicromega.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Refl.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RingMicromega.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Tauto.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_VarMap.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZArith_hints.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZCoeff.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZMicromega.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Zify.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyBool.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyInst.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyPow.cmi
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Ztac.cmi
+lib/ocaml/coq/theories/micromega/DeclConstant.glob
+lib/ocaml/coq/theories/micromega/DeclConstant.v
+lib/ocaml/coq/theories/micromega/DeclConstant.vo
+lib/ocaml/coq/theories/micromega/DeclConstant.vos
+lib/ocaml/coq/theories/micromega/Env.glob
+lib/ocaml/coq/theories/micromega/Env.v
+lib/ocaml/coq/theories/micromega/Env.vo
+lib/ocaml/coq/theories/micromega/Env.vos
+lib/ocaml/coq/theories/micromega/EnvRing.glob
+lib/ocaml/coq/theories/micromega/EnvRing.v
+lib/ocaml/coq/theories/micromega/EnvRing.vo
+lib/ocaml/coq/theories/micromega/EnvRing.vos
+lib/ocaml/coq/theories/micromega/Fourier.glob
+lib/ocaml/coq/theories/micromega/Fourier.v
+lib/ocaml/coq/theories/micromega/Fourier.vo
+lib/ocaml/coq/theories/micromega/Fourier.vos
+lib/ocaml/coq/theories/micromega/Fourier_util.glob
+lib/ocaml/coq/theories/micromega/Fourier_util.v
+lib/ocaml/coq/theories/micromega/Fourier_util.vo
+lib/ocaml/coq/theories/micromega/Fourier_util.vos
+lib/ocaml/coq/theories/micromega/Lia.glob
+lib/ocaml/coq/theories/micromega/Lia.v
+lib/ocaml/coq/theories/micromega/Lia.vo
+lib/ocaml/coq/theories/micromega/Lia.vos
+lib/ocaml/coq/theories/micromega/Lqa.glob
+lib/ocaml/coq/theories/micromega/Lqa.v
+lib/ocaml/coq/theories/micromega/Lqa.vo
+lib/ocaml/coq/theories/micromega/Lqa.vos
+lib/ocaml/coq/theories/micromega/Lra.glob
+lib/ocaml/coq/theories/micromega/Lra.v
+lib/ocaml/coq/theories/micromega/Lra.vo
+lib/ocaml/coq/theories/micromega/Lra.vos
+lib/ocaml/coq/theories/micromega/MExtraction.glob
+lib/ocaml/coq/theories/micromega/MExtraction.v
+lib/ocaml/coq/theories/micromega/MExtraction.vo
+lib/ocaml/coq/theories/micromega/MExtraction.vos
+lib/ocaml/coq/theories/micromega/OrderedRing.glob
+lib/ocaml/coq/theories/micromega/OrderedRing.v
+lib/ocaml/coq/theories/micromega/OrderedRing.vo
+lib/ocaml/coq/theories/micromega/OrderedRing.vos
+lib/ocaml/coq/theories/micromega/Psatz.glob
+lib/ocaml/coq/theories/micromega/Psatz.v
+lib/ocaml/coq/theories/micromega/Psatz.vo
+lib/ocaml/coq/theories/micromega/Psatz.vos
+lib/ocaml/coq/theories/micromega/QMicromega.glob
+lib/ocaml/coq/theories/micromega/QMicromega.v
+lib/ocaml/coq/theories/micromega/QMicromega.vo
+lib/ocaml/coq/theories/micromega/QMicromega.vos
+lib/ocaml/coq/theories/micromega/RMicromega.glob
+lib/ocaml/coq/theories/micromega/RMicromega.v
+lib/ocaml/coq/theories/micromega/RMicromega.vo
+lib/ocaml/coq/theories/micromega/RMicromega.vos
+lib/ocaml/coq/theories/micromega/Refl.glob
+lib/ocaml/coq/theories/micromega/Refl.v
+lib/ocaml/coq/theories/micromega/Refl.vo
+lib/ocaml/coq/theories/micromega/Refl.vos
+lib/ocaml/coq/theories/micromega/RingMicromega.glob
+lib/ocaml/coq/theories/micromega/RingMicromega.v
+lib/ocaml/coq/theories/micromega/RingMicromega.vo
+lib/ocaml/coq/theories/micromega/RingMicromega.vos
+lib/ocaml/coq/theories/micromega/Tauto.glob
+lib/ocaml/coq/theories/micromega/Tauto.v
+lib/ocaml/coq/theories/micromega/Tauto.vo
+lib/ocaml/coq/theories/micromega/Tauto.vos
+lib/ocaml/coq/theories/micromega/VarMap.glob
+lib/ocaml/coq/theories/micromega/VarMap.v
+lib/ocaml/coq/theories/micromega/VarMap.vo
+lib/ocaml/coq/theories/micromega/VarMap.vos
+lib/ocaml/coq/theories/micromega/ZArith_hints.glob
+lib/ocaml/coq/theories/micromega/ZArith_hints.v
+lib/ocaml/coq/theories/micromega/ZArith_hints.vo
+lib/ocaml/coq/theories/micromega/ZArith_hints.vos
+lib/ocaml/coq/theories/micromega/ZCoeff.glob
+lib/ocaml/coq/theories/micromega/ZCoeff.v
+lib/ocaml/coq/theories/micromega/ZCoeff.vo
+lib/ocaml/coq/theories/micromega/ZCoeff.vos
+lib/ocaml/coq/theories/micromega/ZMicromega.glob
+lib/ocaml/coq/theories/micromega/ZMicromega.v
+lib/ocaml/coq/theories/micromega/ZMicromega.vo
+lib/ocaml/coq/theories/micromega/ZMicromega.vos
+lib/ocaml/coq/theories/micromega/Zify.glob
+lib/ocaml/coq/theories/micromega/Zify.v
+lib/ocaml/coq/theories/micromega/Zify.vo
+lib/ocaml/coq/theories/micromega/Zify.vos
+lib/ocaml/coq/theories/micromega/ZifyBool.glob
+lib/ocaml/coq/theories/micromega/ZifyBool.v
+lib/ocaml/coq/theories/micromega/ZifyBool.vo
+lib/ocaml/coq/theories/micromega/ZifyBool.vos
+lib/ocaml/coq/theories/micromega/ZifyClasses.glob
+lib/ocaml/coq/theories/micromega/ZifyClasses.v
+lib/ocaml/coq/theories/micromega/ZifyClasses.vo
+lib/ocaml/coq/theories/micromega/ZifyClasses.vos
+lib/ocaml/coq/theories/micromega/ZifyComparison.glob
+lib/ocaml/coq/theories/micromega/ZifyComparison.v
+lib/ocaml/coq/theories/micromega/ZifyComparison.vo
+lib/ocaml/coq/theories/micromega/ZifyComparison.vos
+lib/ocaml/coq/theories/micromega/ZifyInst.glob
+lib/ocaml/coq/theories/micromega/ZifyInst.v
+lib/ocaml/coq/theories/micromega/ZifyInst.vo
+lib/ocaml/coq/theories/micromega/ZifyInst.vos
+lib/ocaml/coq/theories/micromega/ZifyPow.glob
+lib/ocaml/coq/theories/micromega/ZifyPow.v
+lib/ocaml/coq/theories/micromega/ZifyPow.vo
+lib/ocaml/coq/theories/micromega/ZifyPow.vos
+lib/ocaml/coq/theories/micromega/Ztac.glob
+lib/ocaml/coq/theories/micromega/Ztac.v
+lib/ocaml/coq/theories/micromega/Ztac.vo
+lib/ocaml/coq/theories/micromega/Ztac.vos
+lib/ocaml/coq/theories/nsatz/
+lib/ocaml/coq/theories/nsatz/.coq-native/
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_NsatzTactic.cmi
+lib/ocaml/coq/theories/nsatz/Nsatz.glob
+lib/ocaml/coq/theories/nsatz/Nsatz.v
+lib/ocaml/coq/theories/nsatz/Nsatz.vo
+lib/ocaml/coq/theories/nsatz/Nsatz.vos
+lib/ocaml/coq/theories/nsatz/NsatzTactic.glob
+lib/ocaml/coq/theories/nsatz/NsatzTactic.v
+lib/ocaml/coq/theories/nsatz/NsatzTactic.vo
+lib/ocaml/coq/theories/nsatz/NsatzTactic.vos
+lib/ocaml/coq/theories/omega/
+lib/ocaml/coq/theories/omega/.coq-native/
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_Omega.cmi
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaLemmas.cmi
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaPlugin.cmi
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaTactic.cmi
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_PreOmega.cmi
+lib/ocaml/coq/theories/omega/Omega.glob
+lib/ocaml/coq/theories/omega/Omega.v
+lib/ocaml/coq/theories/omega/Omega.vo
+lib/ocaml/coq/theories/omega/Omega.vos
+lib/ocaml/coq/theories/omega/OmegaLemmas.glob
+lib/ocaml/coq/theories/omega/OmegaLemmas.v
+lib/ocaml/coq/theories/omega/OmegaLemmas.vo
+lib/ocaml/coq/theories/omega/OmegaLemmas.vos
+lib/ocaml/coq/theories/omega/OmegaPlugin.glob
+lib/ocaml/coq/theories/omega/OmegaPlugin.v
+lib/ocaml/coq/theories/omega/OmegaPlugin.vo
+lib/ocaml/coq/theories/omega/OmegaPlugin.vos
+lib/ocaml/coq/theories/omega/OmegaTactic.glob
+lib/ocaml/coq/theories/omega/OmegaTactic.v
+lib/ocaml/coq/theories/omega/OmegaTactic.vo
+lib/ocaml/coq/theories/omega/OmegaTactic.vos
+lib/ocaml/coq/theories/omega/PreOmega.glob
+lib/ocaml/coq/theories/omega/PreOmega.v
+lib/ocaml/coq/theories/omega/PreOmega.vo
+lib/ocaml/coq/theories/omega/PreOmega.vos
+lib/ocaml/coq/theories/rtauto/
+lib/ocaml/coq/theories/rtauto/.coq-native/
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmi
+lib/ocaml/coq/theories/rtauto/Bintree.glob
+lib/ocaml/coq/theories/rtauto/Bintree.v
+lib/ocaml/coq/theories/rtauto/Bintree.vo
+lib/ocaml/coq/theories/rtauto/Bintree.vos
+lib/ocaml/coq/theories/rtauto/Rtauto.glob
+lib/ocaml/coq/theories/rtauto/Rtauto.v
+lib/ocaml/coq/theories/rtauto/Rtauto.vo
+lib/ocaml/coq/theories/rtauto/Rtauto.vos
+lib/ocaml/coq/theories/setoid_ring/
+lib/ocaml/coq/theories/setoid_ring/.coq-native/
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmi
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmi
+lib/ocaml/coq/theories/setoid_ring/Algebra_syntax.glob
+lib/ocaml/coq/theories/setoid_ring/Algebra_syntax.v
+lib/ocaml/coq/theories/setoid_ring/Algebra_syntax.vo
+lib/ocaml/coq/theories/setoid_ring/Algebra_syntax.vos
+lib/ocaml/coq/theories/setoid_ring/ArithRing.glob
+lib/ocaml/coq/theories/setoid_ring/ArithRing.v
+lib/ocaml/coq/theories/setoid_ring/ArithRing.vo
+lib/ocaml/coq/theories/setoid_ring/ArithRing.vos
+lib/ocaml/coq/theories/setoid_ring/BinList.glob
+lib/ocaml/coq/theories/setoid_ring/BinList.v
+lib/ocaml/coq/theories/setoid_ring/BinList.vo
+lib/ocaml/coq/theories/setoid_ring/BinList.vos
+lib/ocaml/coq/theories/setoid_ring/Cring.glob
+lib/ocaml/coq/theories/setoid_ring/Cring.v
+lib/ocaml/coq/theories/setoid_ring/Cring.vo
+lib/ocaml/coq/theories/setoid_ring/Cring.vos
+lib/ocaml/coq/theories/setoid_ring/Field.glob
+lib/ocaml/coq/theories/setoid_ring/Field.v
+lib/ocaml/coq/theories/setoid_ring/Field.vo
+lib/ocaml/coq/theories/setoid_ring/Field.vos
+lib/ocaml/coq/theories/setoid_ring/Field_tac.glob
+lib/ocaml/coq/theories/setoid_ring/Field_tac.v
+lib/ocaml/coq/theories/setoid_ring/Field_tac.vo
+lib/ocaml/coq/theories/setoid_ring/Field_tac.vos
+lib/ocaml/coq/theories/setoid_ring/Field_theory.glob
+lib/ocaml/coq/theories/setoid_ring/Field_theory.v
+lib/ocaml/coq/theories/setoid_ring/Field_theory.vo
+lib/ocaml/coq/theories/setoid_ring/Field_theory.vos
+lib/ocaml/coq/theories/setoid_ring/InitialRing.glob
+lib/ocaml/coq/theories/setoid_ring/InitialRing.v
+lib/ocaml/coq/theories/setoid_ring/InitialRing.vo
+lib/ocaml/coq/theories/setoid_ring/InitialRing.vos
+lib/ocaml/coq/theories/setoid_ring/Integral_domain.glob
+lib/ocaml/coq/theories/setoid_ring/Integral_domain.v
+lib/ocaml/coq/theories/setoid_ring/Integral_domain.vo
+lib/ocaml/coq/theories/setoid_ring/Integral_domain.vos
+lib/ocaml/coq/theories/setoid_ring/NArithRing.glob
+lib/ocaml/coq/theories/setoid_ring/NArithRing.v
+lib/ocaml/coq/theories/setoid_ring/NArithRing.vo
+lib/ocaml/coq/theories/setoid_ring/NArithRing.vos
+lib/ocaml/coq/theories/setoid_ring/Ncring.glob
+lib/ocaml/coq/theories/setoid_ring/Ncring.v
+lib/ocaml/coq/theories/setoid_ring/Ncring.vo
+lib/ocaml/coq/theories/setoid_ring/Ncring.vos
+lib/ocaml/coq/theories/setoid_ring/Ncring_initial.glob
+lib/ocaml/coq/theories/setoid_ring/Ncring_initial.v
+lib/ocaml/coq/theories/setoid_ring/Ncring_initial.vo
+lib/ocaml/coq/theories/setoid_ring/Ncring_initial.vos
+lib/ocaml/coq/theories/setoid_ring/Ncring_polynom.glob
+lib/ocaml/coq/theories/setoid_ring/Ncring_polynom.v
+lib/ocaml/coq/theories/setoid_ring/Ncring_polynom.vo
+lib/ocaml/coq/theories/setoid_ring/Ncring_polynom.vos
+lib/ocaml/coq/theories/setoid_ring/Ncring_tac.glob
+lib/ocaml/coq/theories/setoid_ring/Ncring_tac.v
+lib/ocaml/coq/theories/setoid_ring/Ncring_tac.vo
+lib/ocaml/coq/theories/setoid_ring/Ncring_tac.vos
+lib/ocaml/coq/theories/setoid_ring/RealField.glob
+lib/ocaml/coq/theories/setoid_ring/RealField.v
+lib/ocaml/coq/theories/setoid_ring/RealField.vo
+lib/ocaml/coq/theories/setoid_ring/RealField.vos
+lib/ocaml/coq/theories/setoid_ring/Ring.glob
+lib/ocaml/coq/theories/setoid_ring/Ring.v
+lib/ocaml/coq/theories/setoid_ring/Ring.vo
+lib/ocaml/coq/theories/setoid_ring/Ring.vos
+lib/ocaml/coq/theories/setoid_ring/Ring_base.glob
+lib/ocaml/coq/theories/setoid_ring/Ring_base.v
+lib/ocaml/coq/theories/setoid_ring/Ring_base.vo
+lib/ocaml/coq/theories/setoid_ring/Ring_base.vos
+lib/ocaml/coq/theories/setoid_ring/Ring_polynom.glob
+lib/ocaml/coq/theories/setoid_ring/Ring_polynom.v
+lib/ocaml/coq/theories/setoid_ring/Ring_polynom.vo
+lib/ocaml/coq/theories/setoid_ring/Ring_polynom.vos
+lib/ocaml/coq/theories/setoid_ring/Ring_tac.glob
+lib/ocaml/coq/theories/setoid_ring/Ring_tac.v
+lib/ocaml/coq/theories/setoid_ring/Ring_tac.vo
+lib/ocaml/coq/theories/setoid_ring/Ring_tac.vos
+lib/ocaml/coq/theories/setoid_ring/Ring_theory.glob
+lib/ocaml/coq/theories/setoid_ring/Ring_theory.v
+lib/ocaml/coq/theories/setoid_ring/Ring_theory.vo
+lib/ocaml/coq/theories/setoid_ring/Ring_theory.vos
+lib/ocaml/coq/theories/setoid_ring/Rings_Q.glob
+lib/ocaml/coq/theories/setoid_ring/Rings_Q.v
+lib/ocaml/coq/theories/setoid_ring/Rings_Q.vo
+lib/ocaml/coq/theories/setoid_ring/Rings_Q.vos
+lib/ocaml/coq/theories/setoid_ring/Rings_R.glob
+lib/ocaml/coq/theories/setoid_ring/Rings_R.v
+lib/ocaml/coq/theories/setoid_ring/Rings_R.vo
+lib/ocaml/coq/theories/setoid_ring/Rings_R.vos
+lib/ocaml/coq/theories/setoid_ring/Rings_Z.glob
+lib/ocaml/coq/theories/setoid_ring/Rings_Z.v
+lib/ocaml/coq/theories/setoid_ring/Rings_Z.vo
+lib/ocaml/coq/theories/setoid_ring/Rings_Z.vos
+lib/ocaml/coq/theories/setoid_ring/ZArithRing.glob
+lib/ocaml/coq/theories/setoid_ring/ZArithRing.v
+lib/ocaml/coq/theories/setoid_ring/ZArithRing.vo
+lib/ocaml/coq/theories/setoid_ring/ZArithRing.vos
+lib/ocaml/coq/theories/ssr/
+lib/ocaml/coq/theories/ssr/.coq-native/
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrbool.cmi
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrclasses.cmi
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssreflect.cmi
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrfun.cmi
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmi
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrunder.cmi
+lib/ocaml/coq/theories/ssr/ssrbool.glob
+lib/ocaml/coq/theories/ssr/ssrbool.v
+lib/ocaml/coq/theories/ssr/ssrbool.vo
+lib/ocaml/coq/theories/ssr/ssrbool.vos
+lib/ocaml/coq/theories/ssr/ssrclasses.glob
+lib/ocaml/coq/theories/ssr/ssrclasses.v
+lib/ocaml/coq/theories/ssr/ssrclasses.vo
+lib/ocaml/coq/theories/ssr/ssrclasses.vos
+lib/ocaml/coq/theories/ssr/ssreflect.glob
+lib/ocaml/coq/theories/ssr/ssreflect.v
+lib/ocaml/coq/theories/ssr/ssreflect.vo
+lib/ocaml/coq/theories/ssr/ssreflect.vos
+lib/ocaml/coq/theories/ssr/ssrfun.glob
+lib/ocaml/coq/theories/ssr/ssrfun.v
+lib/ocaml/coq/theories/ssr/ssrfun.vo
+lib/ocaml/coq/theories/ssr/ssrfun.vos
+lib/ocaml/coq/theories/ssr/ssrsetoid.glob
+lib/ocaml/coq/theories/ssr/ssrsetoid.v
+lib/ocaml/coq/theories/ssr/ssrsetoid.vo
+lib/ocaml/coq/theories/ssr/ssrsetoid.vos
+lib/ocaml/coq/theories/ssr/ssrunder.glob
+lib/ocaml/coq/theories/ssr/ssrunder.v
+lib/ocaml/coq/theories/ssr/ssrunder.vo
+lib/ocaml/coq/theories/ssr/ssrunder.vos
+lib/ocaml/coq/theories/ssrmatching/
+lib/ocaml/coq/theories/ssrmatching/.coq-native/
+lib/ocaml/coq/theories/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
+lib/ocaml/coq/theories/ssrmatching/ssrmatching.glob
+lib/ocaml/coq/theories/ssrmatching/ssrmatching.v
+lib/ocaml/coq/theories/ssrmatching/ssrmatching.vo
+lib/ocaml/coq/theories/ssrmatching/ssrmatching.vos
+lib/ocaml/coq/theories/ssrsearch/
+lib/ocaml/coq/theories/ssrsearch/.coq-native/
+lib/ocaml/coq/theories/ssrsearch/.coq-native/NCoq_ssrsearch_ssrsearch.cmi
+lib/ocaml/coq/theories/ssrsearch/ssrsearch.glob
+lib/ocaml/coq/theories/ssrsearch/ssrsearch.v
+lib/ocaml/coq/theories/ssrsearch/ssrsearch.vo
+lib/ocaml/coq/theories/ssrsearch/ssrsearch.vos
lib/ocaml/coq/tools/
lib/ocaml/coq/tools/CoqMakefile.in
lib/ocaml/coq/tools/TimeFileMaker.py
@@ -3225,6 +3367,26 @@ 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/.coq-native/
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmi
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmi
lib/ocaml/coq/user-contrib/Ltac2/Array.glob
lib/ocaml/coq/user-contrib/Ltac2/Array.v
lib/ocaml/coq/user-contrib/Ltac2/Array.vo
@@ -3323,15 +3485,18 @@ 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/comCoercion.cmi
lib/ocaml/coq/vernac/comDefinition.cmi
lib/ocaml/coq/vernac/comFixpoint.cmi
+lib/ocaml/coq/vernac/comHints.cmi
lib/ocaml/coq/vernac/comInductive.cmi
lib/ocaml/coq/vernac/comPrimitive.cmi
lib/ocaml/coq/vernac/comProgramFixpoint.cmi
+lib/ocaml/coq/vernac/comSearch.cmi
+lib/ocaml/coq/vernac/declare.cmi
lib/ocaml/coq/vernac/declareDef.cmi
lib/ocaml/coq/vernac/declareInd.cmi
lib/ocaml/coq/vernac/declareObl.cmi
@@ -3350,12 +3515,15 @@ lib/ocaml/coq/vernac/locality.cmi
lib/ocaml/coq/vernac/metasyntax.cmi
lib/ocaml/coq/vernac/mltop.cmi
lib/ocaml/coq/vernac/obligations.cmi
+lib/ocaml/coq/vernac/pfedit.cmi
lib/ocaml/coq/vernac/ppvernac.cmi
lib/ocaml/coq/vernac/prettyp.cmi
+lib/ocaml/coq/vernac/proof_global.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/retrieveObl.cmi
lib/ocaml/coq/vernac/search.cmi
lib/ocaml/coq/vernac/topfmt.cmi
lib/ocaml/coq/vernac/vernacentries.cmi