math/coq update to 8.13.2p1

Yozo TODA Sat, 08 Jan 2022 22:10:45 -0800

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/NCoqError: bad equal sign escape "=_a" 
at byte 53153 (0xCFA1) of input.
_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

math/coq update to 8.13.2p1

Reply via email to