On Sat, Feb 12, 2022 at 07:22:29PM +0900, Yozo TODA wrote: > 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.
This builds and packages fine without PLIST change on both sparc64 and amd64, thanks! I'll commit your fix. > 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 >
