cpet/openbsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Upgrade math/coq to 8.11.1

Browse Source 
ok daniel@
This commit is contained in:
chrisz 2020-06-01 06:04:50 +00:00
parent adb9a1d809
commit 5ae518c3da
6 changed files with 938 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
math/coq/Makefile
View File

@ -1,8 +1,8 @@
# $OpenBSD: Makefile,v 1.48 2019/10/16 06:40:03 daniel Exp $
# $OpenBSD: Makefile,v 1.49 2020/06/01 06:04:50 chrisz Exp $
COMMENT= proof assistant based on a typed lambda calculus
V= 8.10.0
V= 8.11.1
GH_ACCOUNT = coq
GH_PROJECT = coq
GH_TAGNAME = V${V}
@ -19,7 +19,7 @@ PERMIT_PACKAGE= Yes
WANTLIB += atk-1.0 c cairo cairo-gobject fontconfig freetype gdk-3
WANTLIB += gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0 gtk-3 gtksourceview-3.0
WANTLIB += intl m pango-1.0 pangocairo-1.0 pthread z
WANTLIB += harfbuzz intl m pango-1.0 pangocairo-1.0 pthread z
MODULES= lang/ocaml

4
math/coq/distinfo
View File

@ -1,2 +1,2 @@
SHA256 (coq-8.10.0.tar.gz) = KSxkFiYgxMSCXDI8HHF2LXZOvJzjm9ju6QCFHqymVfU=
SIZE (coq-8.10.0.tar.gz) = 6220333
SHA256 (coq-8.11.1.tar.gz) = mUyfXgsUk8FoKUb2FU74hTyd3rYUkCp/qEA6NlDVN3o=
SIZE (coq-8.11.1.tar.gz) = 6562343

36
math/coq/pkg/PFRAG.dynlink-native
View File

@ -1,4 +1,4 @@
@comment $OpenBSD: PFRAG.dynlink-native,v 1.6 2019/09/20 03:28:33 daniel Exp $
@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
@ -14,6 +14,7 @@
@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmxs
@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmxs
@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmxs
@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
@bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmxs
@ -51,7 +52,15 @@
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Zify.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmxs
@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.cmxs
@bin lib/ocaml/coq/plugins/micromega/micromega_plugin.cmxs
@bin lib/ocaml/coq/plugins/micromega/zify_plugin.cmxs
@bin lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmxs
@bin lib/ocaml/coq/plugins/nsatz/nsatz_plugin.cmxs
@bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmxs
@ -89,11 +98,15 @@
@bin lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmxs
@bin lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmxs
@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmxs
@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.cmxs
@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmxs
@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmxs
@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmxs
@bin lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmxs
@bin lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmxs
@bin lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmxs
@bin lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs
@bin lib/ocaml/coq/plugins/syntax/float_syntax_plugin.cmxs
@bin lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmxs
@bin lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmxs
@bin lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmxs
@ -144,7 +157,7 @@
@bin lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidTactics.cmxs
@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs
@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmxs
@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmxs
@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.cmxs
@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmxs
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmxs
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmxs
@ -167,6 +180,13 @@
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetToFiniteSet.cmxs
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.cmxs
@bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmxs
@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatAxioms.cmxs
@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.cmxs
@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.cmxs
@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.cmxs
@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.cmxs
@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.cmxs
@bin lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmxs
@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmxs
@ -210,6 +230,7 @@
@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmxs
@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FinFun.cmxs
@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.cmxs
@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.cmxs
@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.cmxs
@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_IndefiniteDescription.cmxs
@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_JMeq.cmxs
@ -357,6 +378,13 @@
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ArithProp.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_rel.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_DiscrR.cmxs
@ -398,6 +426,7 @@
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpow_def.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpower.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsigma.cmxs
@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsqrt_def.cmxs
@ -503,7 +532,6 @@
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmxs
@ -516,6 +544,6 @@
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmxs
@bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmxs
@bin lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmxs

127
math/coq/pkg/PFRAG.native
View File

@ -1,4 +1,4 @@
@comment $OpenBSD: PFRAG.native,v 1.6 2019/10/07 06:40:15 chrisz Exp $
@comment $OpenBSD: PFRAG.native,v 1.7 2020/06/01 06:04:50 chrisz Exp $
%%dynlink%%
@bin bin/coqidetop.opt
@bin bin/coqproofworker.opt
@ -65,6 +65,7 @@ lib/ocaml/coq/engine/univProblem.cmx
lib/ocaml/coq/engine/univSubst.cmx
lib/ocaml/coq/engine/univops.cmx
lib/ocaml/coq/gramlib/.pack/gramlib.a
lib/ocaml/coq/gramlib/.pack/gramlib.cmx
lib/ocaml/coq/gramlib/.pack/gramlib.cmxa
lib/ocaml/coq/gramlib/.pack/gramlib__Gramext.cmx
lib/ocaml/coq/gramlib/.pack/gramlib__Grammar.cmx
@ -76,8 +77,8 @@ lib/ocaml/coq/interp/constrexpr.cmx
lib/ocaml/coq/interp/constrexpr_ops.cmx
lib/ocaml/coq/interp/constrextern.cmx
lib/ocaml/coq/interp/constrintern.cmx
lib/ocaml/coq/interp/declare.cmx
lib/ocaml/coq/interp/discharge.cmx
lib/ocaml/coq/interp/decls.cmx
lib/ocaml/coq/interp/deprecation.cmx
lib/ocaml/coq/interp/dumpglob.cmx
lib/ocaml/coq/interp/genintern.cmx
lib/ocaml/coq/interp/impargs.cmx
@ -111,9 +112,11 @@ lib/ocaml/coq/kernel/entries.cmx
lib/ocaml/coq/kernel/environ.cmx
lib/ocaml/coq/kernel/esubst.cmx
lib/ocaml/coq/kernel/evar.cmx
lib/ocaml/coq/kernel/float64.cmx
lib/ocaml/coq/kernel/indTyping.cmx
lib/ocaml/coq/kernel/indtypes.cmx
lib/ocaml/coq/kernel/inductive.cmx
lib/ocaml/coq/kernel/inferCumulativity.cmx
lib/ocaml/coq/kernel/kernel.a
lib/ocaml/coq/kernel/kernel.cmxa
lib/ocaml/coq/kernel/mod_subst.cmx
@ -132,6 +135,7 @@ lib/ocaml/coq/kernel/reduction.cmx
lib/ocaml/coq/kernel/retroknowledge.cmx
lib/ocaml/coq/kernel/retypeops.cmx
lib/ocaml/coq/kernel/safe_typing.cmx
lib/ocaml/coq/kernel/section.cmx
lib/ocaml/coq/kernel/sorts.cmx
lib/ocaml/coq/kernel/subtyping.cmx
lib/ocaml/coq/kernel/term.cmx
@ -174,21 +178,14 @@ lib/ocaml/coq/lib/stateid.cmx
lib/ocaml/coq/lib/system.cmx
lib/ocaml/coq/lib/util.cmx
lib/ocaml/coq/library/coqlib.cmx
lib/ocaml/coq/library/decl_kinds.cmx
lib/ocaml/coq/library/declaremods.cmx
lib/ocaml/coq/library/decls.cmx
lib/ocaml/coq/library/global.cmx
lib/ocaml/coq/library/globnames.cmx
lib/ocaml/coq/library/goptions.cmx
lib/ocaml/coq/library/keys.cmx
lib/ocaml/coq/library/kindops.cmx
lib/ocaml/coq/library/lib.cmx
lib/ocaml/coq/library/libnames.cmx
lib/ocaml/coq/library/libobject.cmx
lib/ocaml/coq/library/library.a
lib/ocaml/coq/library/library.cmx
@static-lib lib/ocaml/coq/library/library.a
lib/ocaml/coq/library/library.cmxa
lib/ocaml/coq/library/loadpath.cmx
lib/ocaml/coq/library/nametab.cmx
lib/ocaml/coq/library/states.cmx
lib/ocaml/coq/library/summary.cmx
@ -241,6 +238,8 @@ lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger
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
@ -291,6 +290,7 @@ 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
lib/ocaml/coq/plugins/funind/gen_principle.cmx
lib/ocaml/coq/plugins/funind/glob_term_to_relation.cmx
lib/ocaml/coq/plugins/funind/glob_termops.cmx
lib/ocaml/coq/plugins/funind/indfun.cmx
@ -371,10 +371,25 @@ 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
lib/ocaml/coq/plugins/micromega/g_micromega.cmx
lib/ocaml/coq/plugins/micromega/g_zify.cmx
lib/ocaml/coq/plugins/micromega/itv.cmx
lib/ocaml/coq/plugins/micromega/mfourier.cmx
lib/ocaml/coq/plugins/micromega/micromega.cmx
@ -388,6 +403,9 @@ lib/ocaml/coq/plugins/micromega/sos.cmx
lib/ocaml/coq/plugins/micromega/sos_lib.cmx
lib/ocaml/coq/plugins/micromega/sos_types.cmx
lib/ocaml/coq/plugins/micromega/vect.cmx
lib/ocaml/coq/plugins/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
@ -476,10 +494,16 @@ 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
@ -499,6 +523,9 @@ lib/ocaml/coq/plugins/ssrmatching/g_ssrmatching.cmx
lib/ocaml/coq/plugins/ssrmatching/ssrmatching.cmx
lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmx
lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.o
lib/ocaml/coq/plugins/syntax/float_syntax.cmx
lib/ocaml/coq/plugins/syntax/float_syntax_plugin.cmx
lib/ocaml/coq/plugins/syntax/float_syntax_plugin.o
lib/ocaml/coq/plugins/syntax/g_numeral.cmx
lib/ocaml/coq/plugins/syntax/g_string.cmx
lib/ocaml/coq/plugins/syntax/int63_syntax.cmx
@ -531,7 +558,7 @@ lib/ocaml/coq/pretyping/glob_term.cmx
lib/ocaml/coq/pretyping/heads.cmx
lib/ocaml/coq/pretyping/indrec.cmx
lib/ocaml/coq/pretyping/inductiveops.cmx
lib/ocaml/coq/pretyping/inferCumulativity.cmx
lib/ocaml/coq/pretyping/keys.cmx
lib/ocaml/coq/pretyping/locus.cmx
lib/ocaml/coq/pretyping/locusops.cmx
lib/ocaml/coq/pretyping/ltac_pretype.cmx
@ -555,7 +582,6 @@ lib/ocaml/coq/pretyping/vnorm.cmx
lib/ocaml/coq/printing/genprint.cmx
lib/ocaml/coq/printing/ppconstr.cmx
lib/ocaml/coq/printing/pputils.cmx
lib/ocaml/coq/printing/prettyp.cmx
lib/ocaml/coq/printing/printer.cmx
lib/ocaml/coq/printing/printing.a
lib/ocaml/coq/printing/printing.cmxa
@ -568,10 +594,8 @@ lib/ocaml/coq/proofs/goal.cmx
lib/ocaml/coq/proofs/goal_select.cmx
lib/ocaml/coq/proofs/logic.cmx
lib/ocaml/coq/proofs/miscprint.cmx
lib/ocaml/coq/proofs/pfedit.cmx
lib/ocaml/coq/proofs/proof.cmx
lib/ocaml/coq/proofs/proof_bullet.cmx
lib/ocaml/coq/proofs/proof_global.cmx
lib/ocaml/coq/proofs/proofs.a
lib/ocaml/coq/proofs/proofs.cmxa
lib/ocaml/coq/proofs/refine.cmx
@ -598,6 +622,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/dn.cmx
lib/ocaml/coq/tactics/dnet.cmx
lib/ocaml/coq/tactics/eauto.cmx
@ -612,7 +638,9 @@ 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
@ -712,8 +740,8 @@ lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.o
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmx
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.o
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmx
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.o
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.cmx
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_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/FSets/.coq-native/NCoq_FSets_FMapAVL.cmx
@ -758,6 +786,20 @@ lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.cmx
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.o
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmx
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.o
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatAxioms.cmx
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatAxioms.o
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.cmx
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.o
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.cmx
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.o
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.cmx
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.o
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.cmx
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.o
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.cmx
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.o
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.cmx
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmx
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.o
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmx
@ -844,6 +886,8 @@ lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FinFun.cmx
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FinFun.o
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.cmx
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.o
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.cmx
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.o
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.cmx
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.o
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_IndefiniteDescription.cmx
@ -1138,6 +1182,20 @@ lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_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
@ -1220,6 +1278,8 @@ lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpower.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpower.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.cmx
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.o
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsigma.cmx
@ -1430,8 +1490,6 @@ lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmx
@ -1456,8 +1514,6 @@ lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
@ -1481,32 +1537,58 @@ 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/g_ltac2.cmx
lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmx
lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.o
lib/ocaml/coq/user-contrib/Ltac2/tac2core.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2dyn.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2entries.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2env.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2extffi.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2ffi.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2intern.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2interp.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2match.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2print.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2quote.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2stdlib.cmx
lib/ocaml/coq/user-contrib/Ltac2/tac2tactics.cmx
lib/ocaml/coq/vernac/assumptions.cmx
lib/ocaml/coq/vernac/attributes.cmx
lib/ocaml/coq/vernac/auto_ind_decl.cmx
lib/ocaml/coq/vernac/canonical.cmx
lib/ocaml/coq/vernac/class.cmx
lib/ocaml/coq/vernac/classes.cmx
lib/ocaml/coq/vernac/comArguments.cmx
lib/ocaml/coq/vernac/comAssumption.cmx
lib/ocaml/coq/vernac/comDefinition.cmx
lib/ocaml/coq/vernac/comFixpoint.cmx
lib/ocaml/coq/vernac/comInductive.cmx
lib/ocaml/coq/vernac/comPrimitive.cmx
lib/ocaml/coq/vernac/comProgramFixpoint.cmx
lib/ocaml/coq/vernac/declareDef.cmx
lib/ocaml/coq/vernac/declareInd.cmx
lib/ocaml/coq/vernac/declareObl.cmx
lib/ocaml/coq/vernac/declareUniv.cmx
lib/ocaml/coq/vernac/declaremods.cmx
lib/ocaml/coq/vernac/egramcoq.cmx
lib/ocaml/coq/vernac/egramml.cmx
lib/ocaml/coq/vernac/explainErr.cmx
lib/ocaml/coq/vernac/g_proofs.cmx
lib/ocaml/coq/vernac/g_vernac.cmx
lib/ocaml/coq/vernac/himsg.cmx
lib/ocaml/coq/vernac/indschemes.cmx
lib/ocaml/coq/vernac/lemmas.cmx
lib/ocaml/coq/vernac/library.cmx
lib/ocaml/coq/vernac/loadpath.cmx
lib/ocaml/coq/vernac/locality.cmx
lib/ocaml/coq/vernac/metasyntax.cmx
lib/ocaml/coq/vernac/mltop.cmx
lib/ocaml/coq/vernac/obligations.cmx
lib/ocaml/coq/vernac/ppvernac.cmx
lib/ocaml/coq/vernac/prettyp.cmx
lib/ocaml/coq/vernac/proof_using.cmx
lib/ocaml/coq/vernac/pvernac.cmx
lib/ocaml/coq/vernac/recLemmas.cmx
lib/ocaml/coq/vernac/record.cmx
lib/ocaml/coq/vernac/search.cmx
lib/ocaml/coq/vernac/topfmt.cmx
@ -1515,5 +1597,6 @@ lib/ocaml/coq/vernac/vernac.cmxa
lib/ocaml/coq/vernac/vernacentries.cmx
lib/ocaml/coq/vernac/vernacexpr.cmx
lib/ocaml/coq/vernac/vernacextend.cmx
lib/ocaml/coq/vernac/vernacinterp.cmx
lib/ocaml/coq/vernac/vernacprop.cmx
lib/ocaml/coq/vernac/vernacstate.cmx

36
math/coq/pkg/PFRAG.no-native
View File

@ -1,4 +1,4 @@
@comment $OpenBSD: PFRAG.no-native,v 1.2 2019/10/07 06:40:15 chrisz Exp $
@comment $OpenBSD: PFRAG.no-native,v 1.3 2020/06/01 06:04:50 chrisz Exp $
lib/ocaml/coq/clib/clib.cma
lib/ocaml/coq/config/config.cma
lib/ocaml/coq/dev/top_printers.cmi
@ -25,6 +25,7 @@ lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.c
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmo
@ -62,7 +63,15 @@ lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Tauto.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Zify.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.cmo
lib/ocaml/coq/plugins/micromega/micromega_plugin.cmo
lib/ocaml/coq/plugins/micromega/zify_plugin.cmo
lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo
lib/ocaml/coq/plugins/nsatz/nsatz_plugin.cmo
lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmo
@ -100,11 +109,15 @@ lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmo
lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmo
lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmo
lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmo
lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.cmo
lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmo
lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmo
lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmo
lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmo
lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmo
lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo
lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmo
lib/ocaml/coq/plugins/syntax/float_syntax_plugin.cmo
lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmo
lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmo
lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmo
@ -160,7 +173,7 @@ lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidDec.cmo
lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidTactics.cmo
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmo
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmo
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmo
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.cmo
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmo
@ -183,6 +196,13 @@ lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetProperties.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetToFiniteSet.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmo
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatAxioms.cmo
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatClass.cmo
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatLemmas.cmo
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_FloatOps.cmo
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_Floats.cmo
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_PrimFloat.cmo
lib/ocaml/coq/theories/Floats/.coq-native/NCoq_Floats_SpecFloat.cmo
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmo
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmo
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmo
@ -226,6 +246,7 @@ lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresent
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FinFun.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_FunctionalExtensionality.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_HLevels.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Hurkens.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_IndefiniteDescription.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_JMeq.cmo
@ -373,6 +394,13 @@ lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_AltSeries.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ArithProp.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_rel.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_DiscrR.cmo
@ -414,6 +442,7 @@ lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rminmax.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpow_def.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rpower.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rprod.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rregisternames.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rseries.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsigma.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rsqrt_def.cmo
@ -519,7 +548,6 @@ lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeuclid.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zlogarithm.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmo
@ -532,8 +560,8 @@ lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmo
lib/ocaml/coq/toplevel/toplevel.cma
lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmo
lib/ocaml/coq/vernac/vernac.cma

792
math/coq/pkg/PLIST
View File

File diff suppressed because it is too large Load Diff