and ping on math/coq update to 8.13.2p1 below, which I confirmed on - amd64 native and - amd64 with modified arch-defines.mk dropping amd64 from OCAML_NATIVE_*
re-attached the diff. btw, the recent riscv64 bulk build report shows the version is coq-8.13.2p1 (it should be 8.13.2p0). why?? > Return-Path: <[email protected]> > From: Yozo TODA <[email protected]> > To: [email protected] > Subject: math/coq update to 8.13.2p1 > Date: Sun, 09 Jan 2022 15:09:45 +0900 > Message-ID: <[email protected]> > > the current math/coq (8.13.2p0) is not packaged on > ocaml non-native architectures, like mips64, riscv64, sparc64, powerpc. > (the recent bulk build reports show that > building success and packaging failure on those architectures.) > > here is an update to adapt to ocaml non-native architectures. > > - entries for native archs only in PLIST moved to PFRAG.native > - entries for non-native archs only in PLIST (with @comment tag) > moved to PFRAG.no-native > - adding @static-lib tag to all .a > - revision bumped though I'm not sure if it should... -- yozo. diff -ur -x CVS /usr/ports/math/coq/Makefile ./coq-8.13.2p1/Makefile --- /usr/ports/math/coq/Makefile Sat Dec 11 09:20:04 2021 +++ ./coq-8.13.2p1/Makefile Sun Jan 9 05:18:04 2022 @@ -8,7 +8,7 @@ GH_TAGNAME = V${V} DISTNAME = ${GH_PROJECT}-${V} WRKDIST = ${WRKDIR}/${GH_PROJECT}-${V} -REVISION = 0 +REVISION = 1 CATEGORIES= math HOMEPAGE= https://coq.inria.fr/ Only in ./coq-8.13.2p1: choi-diff.txt diff -ur -x CVS /usr/ports/math/coq/pkg/PFRAG.native ./coq-8.13.2p1/pkg/PFRAG.native --- /usr/ports/math/coq/pkg/PFRAG.native Sat Dec 11 09:20:04 2021 +++ ./coq-8.13.2p1/pkg/PFRAG.native Sun Jan 9 04:58:36 2022 @@ -1,10 +1,23 @@ @comment $OpenBSD: PFRAG.native,v 1.9 2021/12/04 04:33:45 daniel Exp $ %%dynlink%% +@bin bin/coq-tex +@bin bin/coq_makefile +@bin bin/coqc +@bin bin/coqchk +@bin bin/coqdep +@bin bin/coqdoc +@bin bin/coqide +@bin bin/coqidetop @bin bin/coqidetop.opt @bin bin/coqproofworker.opt @bin bin/coqqueryworker.opt @bin bin/coqtacticworker.opt +@bin bin/coqtop @bin bin/coqtop.opt +@bin bin/coqwc +@bin bin/coqworkmgr +@bin bin/ocamllibdep +@bin bin/votour lib/ocaml/coq/clib/cArray.cmx lib/ocaml/coq/clib/cEphemeron.cmx lib/ocaml/coq/clib/cList.cmx @@ -14,7 +27,7 @@ lib/ocaml/coq/clib/cString.cmx lib/ocaml/coq/clib/cThread.cmx lib/ocaml/coq/clib/cUnix.cmx -lib/ocaml/coq/clib/clib.a +@static-lib lib/ocaml/coq/clib/clib.a lib/ocaml/coq/clib/clib.cmxa lib/ocaml/coq/clib/diff2.cmx lib/ocaml/coq/clib/dyn.cmx @@ -38,11 +51,11 @@ lib/ocaml/coq/clib/unicode.cmx lib/ocaml/coq/clib/unicodetable.cmx lib/ocaml/coq/clib/unionfind.cmx -lib/ocaml/coq/config/config.a +@static-lib lib/ocaml/coq/config/config.a lib/ocaml/coq/config/config.cmxa lib/ocaml/coq/config/coq_config.cmx lib/ocaml/coq/engine/eConstr.cmx -lib/ocaml/coq/engine/engine.a +@static-lib lib/ocaml/coq/engine/engine.a lib/ocaml/coq/engine/engine.cmxa lib/ocaml/coq/engine/evar_kinds.cmx lib/ocaml/coq/engine/evarutil.cmx @@ -61,14 +74,14 @@ 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 +@static-lib 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 lib/ocaml/coq/gramlib/.pack/gramlib__Plexing.cmx lib/ocaml/coq/gramlib/.pack/gramlib__Ploc.cmx -lib/ocaml/coq/ide/coqide/ide.a +@static-lib lib/ocaml/coq/ide/coqide/ide.a lib/ocaml/coq/ide/coqide/ide.cmxa lib/ocaml/coq/interp/constrexpr.cmx lib/ocaml/coq/interp/constrexpr_ops.cmx @@ -80,7 +93,7 @@ lib/ocaml/coq/interp/genintern.cmx lib/ocaml/coq/interp/impargs.cmx lib/ocaml/coq/interp/implicit_quantifiers.cmx -lib/ocaml/coq/interp/interp.a +@static-lib lib/ocaml/coq/interp/interp.a lib/ocaml/coq/interp/interp.cmxa lib/ocaml/coq/interp/modintern.cmx lib/ocaml/coq/interp/notation.cmx @@ -91,6 +104,7 @@ lib/ocaml/coq/interp/smartlocate.cmx lib/ocaml/coq/interp/stdarg.cmx lib/ocaml/coq/interp/syntax_def.cmx +@static-lib lib/ocaml/coq/kernel/byterun/libcoqrun.a lib/ocaml/coq/kernel/cClosure.cmx lib/ocaml/coq/kernel/cPrimitives.cmx lib/ocaml/coq/kernel/constr.cmx @@ -109,7 +123,7 @@ lib/ocaml/coq/kernel/indtypes.cmx lib/ocaml/coq/kernel/inductive.cmx lib/ocaml/coq/kernel/inferCumulativity.cmx -lib/ocaml/coq/kernel/kernel.a +@static-lib lib/ocaml/coq/kernel/kernel.a lib/ocaml/coq/kernel/kernel.cmxa lib/ocaml/coq/kernel/mod_subst.cmx lib/ocaml/coq/kernel/mod_typing.cmx @@ -165,7 +179,7 @@ lib/ocaml/coq/lib/future.cmx lib/ocaml/coq/lib/genarg.cmx lib/ocaml/coq/lib/hook.cmx -lib/ocaml/coq/lib/lib.a +@static-lib lib/ocaml/coq/lib/lib.a lib/ocaml/coq/lib/lib.cmxa lib/ocaml/coq/lib/loc.cmx lib/ocaml/coq/lib/objFile.cmx @@ -194,7 +208,7 @@ lib/ocaml/coq/parsing/g_prim.cmx lib/ocaml/coq/parsing/notation_gram.cmx lib/ocaml/coq/parsing/notgram_ops.cmx -lib/ocaml/coq/parsing/parsing.a +@static-lib lib/ocaml/coq/parsing/parsing.a lib/ocaml/coq/parsing/parsing.cmxa lib/ocaml/coq/parsing/pcoq.cmx lib/ocaml/coq/parsing/ppextend.cmx @@ -283,6 +297,7 @@ lib/ocaml/coq/plugins/ltac/tauto_plugin.o lib/ocaml/coq/plugins/micromega/certificate.cmx lib/ocaml/coq/plugins/micromega/coq_micromega.cmx +@bin lib/ocaml/coq/plugins/micromega/csdpcert lib/ocaml/coq/plugins/micromega/csdpcert.cmx lib/ocaml/coq/plugins/micromega/g_micromega.cmx lib/ocaml/coq/plugins/micromega/g_zify.cmx @@ -382,7 +397,7 @@ lib/ocaml/coq/pretyping/pattern.cmx lib/ocaml/coq/pretyping/patternops.cmx lib/ocaml/coq/pretyping/pretype_errors.cmx -lib/ocaml/coq/pretyping/pretyping.a +@static-lib lib/ocaml/coq/pretyping/pretyping.a lib/ocaml/coq/pretyping/pretyping.cmx lib/ocaml/coq/pretyping/pretyping.cmxa lib/ocaml/coq/pretyping/program.cmx @@ -399,7 +414,7 @@ lib/ocaml/coq/printing/ppconstr.cmx lib/ocaml/coq/printing/pputils.cmx lib/ocaml/coq/printing/printer.cmx -lib/ocaml/coq/printing/printing.a +@static-lib lib/ocaml/coq/printing/printing.a lib/ocaml/coq/printing/printing.cmxa lib/ocaml/coq/printing/proof_diffs.cmx lib/ocaml/coq/proofs/clenv.cmx @@ -410,7 +425,7 @@ lib/ocaml/coq/proofs/miscprint.cmx lib/ocaml/coq/proofs/proof.cmx lib/ocaml/coq/proofs/proof_bullet.cmx -lib/ocaml/coq/proofs/proofs.a +@static-lib lib/ocaml/coq/proofs/proofs.a lib/ocaml/coq/proofs/proofs.cmxa lib/ocaml/coq/proofs/refine.cmx lib/ocaml/coq/proofs/tacmach.cmx @@ -422,7 +437,7 @@ lib/ocaml/coq/stm/partac.cmx lib/ocaml/coq/stm/proofBlockDelimiter.cmx lib/ocaml/coq/stm/spawned.cmx -lib/ocaml/coq/stm/stm.a +@static-lib lib/ocaml/coq/stm/stm.a lib/ocaml/coq/stm/stm.cmx lib/ocaml/coq/stm/stm.cmxa lib/ocaml/coq/stm/tQueue.cmx @@ -456,7 +471,7 @@ lib/ocaml/coq/tactics/redexpr.cmx lib/ocaml/coq/tactics/redops.cmx lib/ocaml/coq/tactics/tacticals.cmx -lib/ocaml/coq/tactics/tactics.a +@static-lib lib/ocaml/coq/tactics/tactics.a lib/ocaml/coq/tactics/tactics.cmx lib/ocaml/coq/tactics/tactics.cmxa lib/ocaml/coq/tactics/term_dnet.cmx @@ -474,7 +489,7 @@ lib/ocaml/coq/toplevel/coqloop.cmx lib/ocaml/coq/toplevel/coqtop.cmx lib/ocaml/coq/toplevel/g_toplevel.cmx -lib/ocaml/coq/toplevel/toplevel.a +@static-lib lib/ocaml/coq/toplevel/toplevel.a lib/ocaml/coq/toplevel/toplevel.cmxa lib/ocaml/coq/toplevel/usage.cmx lib/ocaml/coq/toplevel/vernac.cmx @@ -536,7 +551,7 @@ lib/ocaml/coq/vernac/retrieveObl.cmx lib/ocaml/coq/vernac/search.cmx lib/ocaml/coq/vernac/topfmt.cmx -lib/ocaml/coq/vernac/vernac.a +@static-lib lib/ocaml/coq/vernac/vernac.a lib/ocaml/coq/vernac/vernac.cmxa lib/ocaml/coq/vernac/vernacentries.cmx lib/ocaml/coq/vernac/vernacexpr.cmx diff -ur -x CVS /usr/ports/math/coq/pkg/PFRAG.no-native ./coq-8.13.2p1/pkg/PFRAG.no-native --- /usr/ports/math/coq/pkg/PFRAG.no-native Thu Sep 17 06:13:09 2020 +++ ./coq-8.13.2p1/pkg/PFRAG.no-native Sun Jan 9 05:05:34 2022 @@ -1,10 +1,29 @@ @comment $OpenBSD: PFRAG.no-native,v 1.4 2020/09/16 21:13:09 daniel Exp $ +bin/coq-tex +bin/coq_makefile +bin/coqc +bin/coqchk +bin/coqdep +bin/coqdoc +bin/coqide +bin/coqidetop +bin/coqidetop.byte +bin/coqproofworker.byte +bin/coqqueryworker.byte +bin/coqtacticworker.byte +bin/coqtop +bin/coqtop.byte +bin/coqwc +bin/coqworkmgr +bin/ocamllibdep +bin/votour lib/ocaml/coq/clib/clib.cma lib/ocaml/coq/config/config.cma lib/ocaml/coq/dev/top_printers.cmi +@so lib/ocaml/coq/dllcoqrun.so lib/ocaml/coq/engine/engine.cma lib/ocaml/coq/gramlib/.pack/gramlib.cma -lib/ocaml/coq/ide/ide.cma +lib/ocaml/coq/ide/coqide/ide.cma lib/ocaml/coq/interp/interp.cma lib/ocaml/coq/kernel/kernel.cma lib/ocaml/coq/lib/lib.cma @@ -18,595 +37,24 @@ lib/ocaml/coq/plugins/funind/recdef_plugin.cmo lib/ocaml/coq/plugins/ltac/ltac_plugin.cmo lib/ocaml/coq/plugins/ltac/tauto_plugin.cmo +lib/ocaml/coq/plugins/micromega/csdpcert lib/ocaml/coq/plugins/micromega/micromega_plugin.cmo lib/ocaml/coq/plugins/micromega/zify_plugin.cmo lib/ocaml/coq/plugins/nsatz/nsatz_plugin.cmo lib/ocaml/coq/plugins/omega/omega_plugin.cmo +lib/ocaml/coq/plugins/ring/ring_plugin.cmo lib/ocaml/coq/plugins/rtauto/rtauto_plugin.cmo -lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmo lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmo lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmo lib/ocaml/coq/plugins/ssrsearch/ssrsearch_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 -lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmo +lib/ocaml/coq/plugins/syntax/number_string_notation_plugin.cmo lib/ocaml/coq/pretyping/pretyping.cma lib/ocaml/coq/printing/printing.cma lib/ocaml/coq/proofs/proofs.cma lib/ocaml/coq/stm/stm.cma lib/ocaml/coq/tactics/tactics.cma -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Arith_base.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Between.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Bool_nat.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Compare.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Compare_dec.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Div2.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_EqNat.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Euclid.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Even.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Factorial.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Gt.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Le.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Lt.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Max.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Min.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Minus.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Mult.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_PeanoNat.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Peano_dec.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Plus.cmo -lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Wf_nat.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bool.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolEq.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolOrder.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bvector.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_DecBool.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_IfProp.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Sumbool.cmo -lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Zerob.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_CEquivalence.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_CMorphisms.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_CRelationClasses.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_DecidableClass.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_EquivDec.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_Equivalence.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_Init.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_Morphisms.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_Morphisms_Prop.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_Morphisms_Relations.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_RelationClasses.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_RelationPairs.cmo -lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidClass.cmo -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_Coq811.cmo -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq812.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFullAVL.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapInterface.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapList.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapPositive.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapWeakList.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMaps.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetAVL.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetBridge.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetCompat.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetDecide.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetEqProperties.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetFacts.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetInterface.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetList.cmo -lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetPositive.cmo -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 -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Hexadecimal.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic_Type.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Ltac.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Nat.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Notations.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Numeral.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Peano.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Prelude.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmo -lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_List.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_ListDec.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_ListSet.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_ListTactics.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_SetoidList.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_SetoidPermutation.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_StreamMemo.cmo -lib/ocaml/coq/theories/Lists/.coq-native/NCoq_Lists_Streams.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Berardi.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ChoiceFacts.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Classical.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ClassicalChoice.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ClassicalDescription.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ClassicalEpsilon.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ClassicalFacts.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ClassicalUniqueChoice.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Classical_Pred_Type.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Classical_Prop.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ConstructiveEpsilon.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Decidable.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Description.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Diaconescu.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Epsilon.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_EqdepFacts.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.cmo -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 -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevance.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFacts.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmo -lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetAVL.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetDecide.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetEqProperties.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetFacts.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetGenTree.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetInterface.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetList.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetPositive.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetProperties.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetRBT.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetToFiniteSet.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetWeakList.cmo -lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSets.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_BinNat.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_BinNatDef.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_NArith.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ndec.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ndigits.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ndist.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ndiv_def.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ngcd_def.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nnat.cmo -lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalQ.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalFacts.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalN.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalNat.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalPos.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalQ.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalString.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalZ.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmo -lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Int31.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmo -lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAddOrder.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAxioms.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZBase.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZBits.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZDivEucl.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZDivFloor.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZDivTrunc.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZGcd.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZLcm.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZLt.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZMaxMin.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZMul.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZMulOrder.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZParity.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZPow.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZProperties.cmo -lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZSgnAbs.cmo -lib/ocaml/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmo -lib/ocaml/coq/theories/Numbers/Integer/NatPairs/.coq-native/NCoq_Numbers_Integer_NatPairs_ZNatPairs.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZAdd.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZAddOrder.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZAxioms.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZBase.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZBits.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZDiv.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZDomain.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZGcd.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZLog.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZMul.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZMulOrder.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZOrder.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZParity.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZPow.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZProperties.cmo -lib/ocaml/coq/theories/Numbers/NatInt/.coq-native/NCoq_Numbers_NatInt_NZSqrt.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NAdd.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NAddOrder.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NAxioms.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NBase.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NBits.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NDefOps.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NDiv.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NGcd.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NIso.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NLcm.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NLog.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NMaxMin.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NMulOrder.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NOrder.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NParity.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NPow.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NProperties.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NSqrt.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NStrongRec.cmo -lib/ocaml/coq/theories/Numbers/Natural/Abstract/.coq-native/NCoq_Numbers_Natural_Abstract_NSub.cmo -lib/ocaml/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmo -lib/ocaml/coq/theories/Numbers/Natural/Peano/.coq-native/NCoq_Numbers_Natural_Peano_NPeano.cmo -lib/ocaml/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmo -lib/ocaml/coq/theories/PArith/.coq-native/NCoq_PArith_BinPosDef.cmo -lib/ocaml/coq/theories/PArith/.coq-native/NCoq_PArith_PArith.cmo -lib/ocaml/coq/theories/PArith/.coq-native/NCoq_PArith_POrderedType.cmo -lib/ocaml/coq/theories/PArith/.coq-native/NCoq_PArith_Pnat.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Basics.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Combinators.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Equality.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Program.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Subset.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Syntax.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Tactics.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Utils.cmo -lib/ocaml/coq/theories/Program/.coq-native/NCoq_Program_Wf.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_QArith.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_QArith_base.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_QOrderedType.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qfield.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qminmax.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qpower.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qreals.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qreduction.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qring.cmo -lib/ocaml/coq/theories/QArith/.coq-native/NCoq_QArith_Qround.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Alembert.cmo -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_ClassicalConstructiveReals.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.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 -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Exp_prop.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Integration.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_MVT.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Machin.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_NewtonInt.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_PSeries_reg.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_PartSum.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_RIneq.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_RList.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ROrderedType.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_R_Ifp.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_R_sqr.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_R_sqrt.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ranalysis.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ranalysis1.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ranalysis2.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ranalysis3.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ranalysis4.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ranalysis5.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ranalysis_reg.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Ratan.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Raxioms.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rbase.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rbasic_fun.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rcomplete.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rdefinitions.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rderiv.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Reals.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rfunctions.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rgeom.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_RiemannInt.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_RiemannInt_SF.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rlimit.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rlogic.cmo -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 -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtopology.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo1.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_alt.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_calc.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_facts.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitRmult.cmo -lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Sqrt_reg.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveAbs.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLUB.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLimits.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveMinMax.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructivePower.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveReals.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.cmo -lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveSum.cmo -lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.cmo -lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyReals.cmo -lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.cmo -lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveRcomplete.cmo -lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Operators_Properties.cmo -lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Definitions.cmo -lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Operators.cmo -lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relations.cmo -lib/ocaml/coq/theories/Setoids/.coq-native/NCoq_Setoids_Setoid.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Classical_sets.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Constructive_sets.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Cpo.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Ensembles.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Finite_sets.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Finite_sets_facts.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Image.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Infinite_sets.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Integers.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Multiset.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Partial_Order.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Permut.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Powerset.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Powerset_Classical_facts.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Powerset_facts.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_1.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_1_facts.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_2.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_2_facts.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3_facts.cmo -lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Uniset.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_CPermutation.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Mergesort.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_PermutEq.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_PermutSetoid.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Permutation.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorted.cmo -lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorting.cmo -lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmo -lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmo -lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmo -lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmo -lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmo -lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmo -lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableType.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableTypeEx.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_Equalities.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_EqualitiesFacts.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_GenericMinMax.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrderedType.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrderedTypeAlt.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrderedTypeEx.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_Orders.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrdersAlt.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrdersEx.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrdersFacts.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrdersLists.cmo -lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_OrdersTac.cmo -lib/ocaml/coq/theories/Unicode/.coq-native/NCoq_Unicode_Utf8.cmo -lib/ocaml/coq/theories/Unicode/.coq-native/NCoq_Unicode_Utf8_core.cmo -lib/ocaml/coq/theories/Vectors/.coq-native/NCoq_Vectors_Fin.cmo -lib/ocaml/coq/theories/Vectors/.coq-native/NCoq_Vectors_Vector.cmo -lib/ocaml/coq/theories/Vectors/.coq-native/NCoq_Vectors_VectorDef.cmo -lib/ocaml/coq/theories/Vectors/.coq-native/NCoq_Vectors_VectorEq.cmo -lib/ocaml/coq/theories/Vectors/.coq-native/NCoq_Vectors_VectorSpec.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Disjoint_Union.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Inclusion.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Inverse_Image.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Lexicographic_Exponentiation.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Lexicographic_Product.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Transitive_Closure.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Union.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Well_Ordering.cmo -lib/ocaml/coq/theories/Wellfounded/.coq-native/NCoq_Wellfounded_Wellfounded.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_BinInt.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_BinIntDef.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Int.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Wf_Z.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_base.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_dec.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zabs.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zbool.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcompare.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcomplements.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdigits.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdiv.cmo -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_Zmax.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmisc.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znat.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znumtheory.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zorder.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.cmo -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_Zwf.cmo -lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmo -lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Algebra.cmo -lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Btauto.cmo -lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Reflect.cmo -lib/ocaml/coq/theories/derive/.coq-native/NCoq_derive_Derive.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNativeString.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmo -lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_Extraction.cmo -lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_FunInd.cmo -lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_Recdef.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_DeclConstant.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Env.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_EnvRing.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier_util.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lia.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lqa.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lra.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_MExtraction.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Psatz.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_QMicromega.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RMicromega.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Refl.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RingMicromega.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Tauto.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_VarMap.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZArith_hints.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZCoeff.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZMicromega.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Zify.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyBool.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyInst.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyPow.cmo -lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Ztac.cmo -lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo -lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_NsatzTactic.cmo -lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_Omega.cmo -lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaLemmas.cmo -lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaPlugin.cmo -lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaTactic.cmo -lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_PreOmega.cmo -lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Bintree.cmo -lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmo -lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmo -lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrbool.cmo -lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrclasses.cmo -lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssreflect.cmo -lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrfun.cmo -lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmo -lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrunder.cmo -lib/ocaml/coq/theories/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo -lib/ocaml/coq/theories/ssrsearch/.coq-native/NCoq_ssrsearch_ssrsearch.cmo lib/ocaml/coq/toplevel/toplevel.cma -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmo -lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmo lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmo lib/ocaml/coq/vernac/vernac.cma diff -ur -x CVS /usr/ports/math/coq/pkg/PLIST ./coq-8.13.2p1/pkg/PLIST --- /usr/ports/math/coq/pkg/PLIST Sat Dec 11 09:20:04 2021 +++ ./coq-8.13.2p1/pkg/PLIST Sun Jan 9 05:02:45 2022 @@ -1,25 +1,7 @@ @comment $OpenBSD: PLIST,v 1.17 2021/12/04 04:33:45 daniel Exp $ %%native%% !%%native%% -@bin bin/coq-tex -@bin bin/coq_makefile -@bin bin/coqc -@bin bin/coqchk -@bin bin/coqdep -@bin bin/coqdoc -@bin bin/coqide -@bin bin/coqidetop -@comment bin/coqidetop.byte bin/coqpp -@comment bin/coqproofworker.byte -@comment bin/coqqueryworker.byte -@comment bin/coqtacticworker.byte -@bin bin/coqtop -@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/ @@ -62,10 +44,9 @@ lib/ocaml/coq/coqpp/coqpp_parse.cmi lib/ocaml/coq/coqpp/coqpp_parser.cmi lib/ocaml/coq/dev/ -@comment lib/ocaml/coq/dllcoqrun.so -lib/ocaml/coq/doc/ -lib/ocaml/coq/doc/tools/ -lib/ocaml/coq/doc/tools/docgram/ +@comment lib/ocaml/coq/doc/ +@comment lib/ocaml/coq/doc/tools/ +@comment lib/ocaml/coq/doc/tools/docgram/ lib/ocaml/coq/engine/ lib/ocaml/coq/engine/eConstr.cmi lib/ocaml/coq/engine/evar_kinds.cmi @@ -149,7 +130,6 @@ lib/ocaml/coq/kernel/ lib/ocaml/coq/kernel/byterun/ @so lib/ocaml/coq/kernel/byterun/dllcoqrun.so -@comment lib/ocaml/coq/kernel/byterun/libcoqrun.a lib/ocaml/coq/kernel/cClosure.cmi lib/ocaml/coq/kernel/cPrimitives.cmi lib/ocaml/coq/kernel/constr.cmi @@ -324,7 +304,6 @@ lib/ocaml/coq/plugins/micromega/ lib/ocaml/coq/plugins/micromega/certificate.cmi lib/ocaml/coq/plugins/micromega/coq_micromega.cmi -@bin lib/ocaml/coq/plugins/micromega/csdpcert lib/ocaml/coq/plugins/micromega/csdpcert.cmi lib/ocaml/coq/plugins/micromega/g_micromega.cmi lib/ocaml/coq/plugins/micromega/itv.cmi
