rocq-core-9.2.0-2.fc45 RPM for x86_64

From Fedora Rawhide for x86_64 / r

Rocq is a formal proof management system.  It provides a formal language to
write mathematical definitions, executable algorithms and theorems together
with an environment for semi-interactive development of machine-checked proofs.

This package includes the Rocq prelude, that is loaded automatically
by Rocq in every .v file, as well as other modules bound to the
Corelib.* and Ltac2.* namespaces.

Provides

• rocq-core
• coq
• ocaml(NCorelib_Array_ArrayAxioms)
• ocaml(NCorelib_Array_PrimArray)
• ocaml(NCorelib_BinNums_IntDef)
• ocaml(NCorelib_BinNums_NatDef)
• ocaml(NCorelib_BinNums_PosDef)
• ocaml(NCorelib_Classes_CMorphisms)
• ocaml(NCorelib_Classes_CRelationClasses)
• ocaml(NCorelib_Classes_Equivalence)
• ocaml(NCorelib_Classes_Init)
• ocaml(NCorelib_Classes_Morphisms)
• ocaml(NCorelib_Classes_Morphisms_Prop)
• ocaml(NCorelib_Classes_RelationClasses)
• ocaml(NCorelib_Classes_SetoidTactics)
• ocaml(NCorelib_Compat_Coq818)
• ocaml(NCorelib_Compat_Coq819)
• ocaml(NCorelib_Compat_Coq820)
• ocaml(NCorelib_Compat_Rocq90)
• ocaml(NCorelib_Compat_Rocq91)
• ocaml(NCorelib_Floats_FloatAxioms)
• ocaml(NCorelib_Floats_FloatClass)
• ocaml(NCorelib_Floats_FloatOps)
• ocaml(NCorelib_Floats_PrimFloat)
• ocaml(NCorelib_Floats_SpecFloat)
• ocaml(NCorelib_Init_Byte)
• ocaml(NCorelib_Init_Datatypes)
• ocaml(NCorelib_Init_Decimal)
• ocaml(NCorelib_Init_Equality)
• ocaml(NCorelib_Init_Hexadecimal)
• ocaml(NCorelib_Init_Logic)
• ocaml(NCorelib_Init_Ltac)
• ocaml(NCorelib_Init_Nat)
• ocaml(NCorelib_Init_Notations)
• ocaml(NCorelib_Init_Number)
• ocaml(NCorelib_Init_Peano)
• ocaml(NCorelib_Init_Prelude)
• ocaml(NCorelib_Init_Specif)
• ocaml(NCorelib_Init_Sumbool)
• ocaml(NCorelib_Init_Tactics)
• ocaml(NCorelib_Init_Tauto)
• ocaml(NCorelib_Init_Wf)
• ocaml(NCorelib_Lists_ListDef)
• ocaml(NCorelib_Numbers_BinNums)
• ocaml(NCorelib_Numbers_Cyclic_Int63_CarryType)
• ocaml(NCorelib_Numbers_Cyclic_Int63_PrimInt63)
• ocaml(NCorelib_Numbers_Cyclic_Int63_Sint63Axioms)
• ocaml(NCorelib_Numbers_Cyclic_Int63_Uint63Axioms)
• ocaml(NCorelib_Program_Basics)
• ocaml(NCorelib_Program_Tactics)
• ocaml(NCorelib_Program_Utils)
• ocaml(NCorelib_Program_Wf)
• ocaml(NCorelib_Relations_Relation_Definitions)
• ocaml(NCorelib_Setoids_Setoid)
• ocaml(NCorelib_Strings_PrimString)
• ocaml(NCorelib_Strings_PrimStringAxioms)
• ocaml(NCorelib_derive_Derive)
• ocaml(NCorelib_extraction_ExtrHaskellBasic)
• ocaml(NCorelib_extraction_ExtrOcamlBasic)
• ocaml(NCorelib_extraction_Extraction)
• ocaml(NCorelib_ssr_ssrbool)
• ocaml(NCorelib_ssr_ssrclasses)
• ocaml(NCorelib_ssr_ssreflect)
• ocaml(NCorelib_ssr_ssrfun)
• ocaml(NCorelib_ssr_ssrsetoid)
• ocaml(NCorelib_ssr_ssrunder)
• ocaml(NCorelib_ssrmatching_ssrmatching)
• ocaml(NLtac2_Array)
• ocaml(NLtac2_Bool)
• ocaml(NLtac2_Char)
• ocaml(NLtac2_Compat_Coq818)
• ocaml(NLtac2_Compat_Coq819)
• ocaml(NLtac2_Constant)
• ocaml(NLtac2_Constr)
• ocaml(NLtac2_Constructor)
• ocaml(NLtac2_Control)
• ocaml(NLtac2_Env)
• ocaml(NLtac2_Evar)
• ocaml(NLtac2_FMap)
• ocaml(NLtac2_FSet)
• ocaml(NLtac2_Float)
• ocaml(NLtac2_Fresh)
• ocaml(NLtac2_Ident)
• ocaml(NLtac2_Ind)
• ocaml(NLtac2_Init)
• ocaml(NLtac2_Int)
• ocaml(NLtac2_Lazy)
• ocaml(NLtac2_List)
• ocaml(NLtac2_Ltac1)
• ocaml(NLtac2_Ltac1CompatNotations)
• ocaml(NLtac2_Ltac2)
• ocaml(NLtac2_Message)
• ocaml(NLtac2_Meta)
• ocaml(NLtac2_Module)
• ocaml(NLtac2_Notations)
• ocaml(NLtac2_Option)
• ocaml(NLtac2_Pattern)
• ocaml(NLtac2_Printf)
• ocaml(NLtac2_Proj)
• ocaml(NLtac2_Pstring)
• ocaml(NLtac2_RedFlags)
• ocaml(NLtac2_Ref)
• ocaml(NLtac2_Reference)
• ocaml(NLtac2_Rewrite)
• ocaml(NLtac2_Std)
• ocaml(NLtac2_String)
• ocaml(NLtac2_TransparentState)
• ocaml(NLtac2_Uint63)
• ocaml(NLtac2_Unification)
• rocq-core(x86-64)

Requires

• ocaml(AcyclicGraph) = ce0c9bd3b201f36ced3b625547d079cc
• ocaml(Boot) = f4d97e713a6c402b8fdc05370892f9c0
• ocaml(Boot__Env) = 40f0e5eeb9772e25a9a23798b7d8af94
• ocaml(Boot__Usage) = f36579e92f4ad02ef5bcba239cef2a95
• ocaml(CAst) = 385fa113703c5cc4b2aac40286c513fd
• ocaml(CClosure) = c9285ea5ffdb8bdec971594e8314e54e
• ocaml(CDebug) = 450ef430d34972b281d4a0e01c850b22
• ocaml(CEphemeron) = c8ec9684138eae94f9ada62543edc0cf
• ocaml(CList) = 0882adb5c5a227e92b2a3a07183e83e6
• ocaml(CMap) = 8a56e198dd6e5a2f9a7b38c2abb1db60
• ocaml(CPrimitives) = 83560da1532dd9fe868cd437983f2e90
• ocaml(CSet) = 29dbd5eead5024c34a1593aadc924d05
• ocaml(CSig) = 26c574d98d011351d971fbd27b9e8b09
• ocaml(CString) = 13b232370c07ef859b331ccc579a183e
• ocaml(CUnix) = 57f5c9158430515b08a4f211723449fc
• ocaml(CWarnings) = 02eebb5695bd1c2c73b7403691062f22
• ocaml(CamlinternalFormatBasics) = 5cba8713ea434e43a50cd422bda47dda
• ocaml(CamlinternalLazy) = 39aa2e9bf7e25b383556f7748b45c72f
• ocaml(Constr) = 9dadde4182692178010a5198af7d913d
• ocaml(Context) = 4b00288eda58099636359976fb690e6b
• ocaml(Conv_oracle) = 483252ac95333754084890d1b56ffc12
• ocaml(Conversion) = 986b7f42c233728daaf352167dda80f7
• ocaml(Cooking) = e46065361836085992529aba620b7dee
• ocaml(Coq_config) = e637fe8ad1c7762085636f5615d35265
• ocaml(Declarations) = 6565fde992dda095d8a344bbd4f7bb40
• ocaml(Environ) = 333a65beee3fab8db793cb06ef9fa139
• ocaml(Esubst) = bd721a72d48ad134792fe495afd30ce6
• ocaml(Evar) = ac2e8f4bba960dd78af41a3bad3f3238
• ocaml(Exninfo) = 8b1c1f5a459f237a6eefbdc05e3c0c3a
• ocaml(Float64) = 5f3685872420eb559610ca8cc70758b1
• ocaml(Genlambda) = 183fb5c4fdf9f526727a384411b1c16b
• ocaml(Hashcons) = 6f55751bed5c20cdac5336a90cab41b5
• ocaml(Hashset) = 8d0a557f8649d7eeae2802c1e49e95e0
• ocaml(Int) = 6d90e5f7db4cb744e44df7510c8a0c87
• ocaml(Loc) = 2af96156e647600dba688160d767ed1d
• ocaml(Mod_declarations) = a4bb92788732bff3137cb6e05650d81d
• ocaml(Mod_subst) = 2ae3a7fa4a4cd916f9fa48e07e85ffb6
• ocaml(NCorelib_BinNums_IntDef) = b603438853bd33f049a94783a30c6333
• ocaml(NCorelib_BinNums_NatDef) = e1d2676566459d9123cd2aac6bd0a969
• ocaml(NCorelib_BinNums_PosDef) = d83ca7ec7baf13fb3c9fe723f0008fbc
• ocaml(NCorelib_Classes_CRelationClasses) = 1cd594a0971c14ce5438e63b23348c8f
• ocaml(NCorelib_Classes_Morphisms) = 277653331b414ec4b44bfce9c4a1ec3f
• ocaml(NCorelib_Classes_RelationClasses) = f39f6c6c0cd9c148b55b6c54449a180b
• ocaml(NCorelib_Floats_FloatClass) = f8d75ccafd44a389e6eef768f3b08f06
• ocaml(NCorelib_Floats_FloatOps) = ab199041b21f0eef9191a78de20756a1
• ocaml(NCorelib_Floats_PrimFloat) = 2386385e28418d1689999d7d14cb10d5
• ocaml(NCorelib_Floats_SpecFloat) = b0181d79b0cabd77104ca87bd5495957
• ocaml(NCorelib_Init_Datatypes) = 79ff2757e7b22f0a8aa1a1726c654edd
• ocaml(NCorelib_Init_Decimal) = 9e2d289a76542fc1d720d011cd03a956
• ocaml(NCorelib_Init_Hexadecimal) = 66e4f7a8a2eba1fc6eb9205898a8e82d
• ocaml(NCorelib_Init_Logic) = 7825e48c2f4d7d86e62a56573922492d
• ocaml(NCorelib_Init_Nat) = 3f2ce24f451fcb1383719d75f6960aa6
• ocaml(NCorelib_Init_Number) = e8f09ee5997f984c907e39d2deb0bed4
• ocaml(NCorelib_Init_Specif) = 935b3304f6522587c83ed0ef535feb29
• ocaml(NCorelib_Init_Wf) = 206ec0fa9a59dad1d56c42d8b858ddef
• ocaml(NCorelib_Lists_ListDef) = dc3bae3fa24c9e5cf118836392ef783a
• ocaml(NCorelib_Numbers_BinNums) = 2ac25e4043f9b5264a86a748432f29a1
• ocaml(NCorelib_Numbers_Cyclic_Int63_CarryType) = ae40d6e12559145cef549ba3688d5c3c
• ocaml(NCorelib_Numbers_Cyclic_Int63_PrimInt63) = a7442e184c993046561138290082d6c5
• ocaml(NCorelib_Numbers_Cyclic_Int63_Uint63Axioms) = 45032477362e265611c2429f3708e6ac
• ocaml(NCorelib_Program_Basics) = e75a9d1e92f8b5e3d83e77be393b2cc5
• ocaml(NCorelib_Strings_PrimString) = 3160fcda7db60564adc5b142a858d66a
• ocaml(NCorelib_ssr_ssreflect) = 84a95b7216acc4ea50925f9363333885
• ocaml(NCorelib_ssr_ssrfun) = 73955f91ede01bfd7a535e095c0e3c4f
• ocaml(NCorelib_ssr_ssrunder) = 4e944bf8839f5e76352dd4a5b786d1ee
• ocaml(Names) = 148e9d5d2ba1c0a16d00e80d17fd6535
• ocaml(Nativecode) = fe56e91fd3a3c9864c5da07bd55882cd
• ocaml(Nativeconv) = fa8552c1d9c0b14005df307dc194784c
• ocaml(Nativelib) = f21908f71586fb123e1744044a7eac16
• ocaml(Nativevalues) = 6c52af047b1da04f7d32b88ffb5aa655
• ocaml(ObjFile) = 2c13d8ad4646786734c912359c91a0ba
• ocaml(Opaqueproof) = 1aadd50f1d0bea28189a01fd2570f17f
• ocaml(PConstraints) = d417f36ebf2f64643590cc1369e98261
• ocaml(Parray) = c91aee66f0a62119d8324dff17c9a4b8
• ocaml(Partial_subst) = 293aaba2bff2483262e01afda5396a0a
• ocaml(Pp) = 2c38bf624e0ffbba3e2389beec2065bb
• ocaml(Predicate) = 0c221b82d5cdae9cbeeea482f4dc5d9d
• ocaml(Pstring) = a4657eedcbcee758e124eaf4bdbd082f
• ocaml(QGraph) = a0f3170eb602a676cfd042aebb11b569
• ocaml(Quickfix) = a99365c9ce5cdad164252c7e05e04016
• ocaml(Range) = fd4c0f33c700ee2d3bc0cd2a9504ce03
• ocaml(RedFlags) = e0b3bd029593004b900aaa26937f4f32
• ocaml(Retroknowledge) = 0ff314acfded9b1ae195b6f6a6d53479
• ocaml(Rtree) = cc005cc024069460855d05480a7fb91f
• ocaml(SList) = 4bc007590fe5ee6fa7d6f33af5ae66c9
• ocaml(Sorts) = bff26bd11f9b46fa49d5f70ea2679f4d
• ocaml(Stdlib) = 5debf066d2f080eabc33d8b71099252f
• ocaml(Stdlib__Bigarray) = 904d1271afeb602c556bf1e0f0f8809c
• ocaml(Stdlib__Buffer) = c0940caa52bfb8d306ed2ca69af87ed6
• ocaml(Stdlib__Complex) = 7a66a05174368cc820464e6c12a3693c
• ocaml(Stdlib__Digest) = 2b70a92ff90913804cdc1343b1592e27
• ocaml(Stdlib__Domain) = d11ad689f3e35d9892101961a1201121
• ocaml(Stdlib__Either) = e4e548dbb128df23a9325d9cba39fc2f
• ocaml(Stdlib__Format) = 5b2f2a54d0831d599db87620d18b8ca1
• ocaml(Stdlib__Int32) = 6583ec691ad5b5d0403bb4dba14ff95a
• ocaml(Stdlib__Int64) = 6c1bd23e0da837071a98f3330e9f1242
• ocaml(Stdlib__Lazy) = 9888b2ba7f344f43c41116cffda5081a
• ocaml(Stdlib__List) = 81a27a0a9af489e91fa1d99f325067c2
• ocaml(Stdlib__Map) = a9944feda56cab2432578db95de546a3
• ocaml(Stdlib__Obj) = 26b40efd5c9a30f8c9c87c6133b5adbf
• ocaml(Stdlib__Seq) = b55b17884ef0dff6295517debe21f111
• ocaml(Stdlib__Set) = 878d51b56f0f7be3121d17ee49b6ece5
• ocaml(Stdlib__String) = 10f6a338df78df4f5987192086ffa3c9
• ocaml(Stdlib__Sys) = fb4c43482366ca204eebf7f3838d5a55
• ocaml(Stdlib__Uchar) = ffc32f05aeea05f14986ec532040e8b1
• ocaml(TransparentState) = 492fb566dd40324c3ac3c40c6a3eac3d
• ocaml(UGraph) = fd4fb27f84eb29897851009e5afeff5d
• ocaml(UVars) = 9173bf68da786badcc850fad917fa866
• ocaml(Uint63) = 9876a8b5a0ed526272adc8f269a8c8ab
• ocaml(Univ) = 3c2fe6798a168ef754f3af6682208113
• ocaml(Unix) = a088c1880ec9ae11d7b8ef8cdf3a21d7
• ocaml(Util) = 219a82943a407209300fd2eca83af94c
• ocaml(Values) = 45cafd9cf84d283e233b8fe611baf6fe
• ocaml(Vars) = 56a181095688f99c5303624a612df3fe
• ocaml(Vmbytecodes) = d2a8610fa6ecb2844faea10b4e8fe16a
• ocaml(Vmemitcodes) = 1ea3ce15bb933df35ea9a0fc0ab45c04
• ocaml(Vmlibrary) = 1abf8f71db3617eab8b38acc264c0602
• ocaml(Vmvalues) = c5815fac5c13273b8822d1d266db6182
• rocq-runtime(x86-64) = 9.2.0-2.fc45
• rpmlib(CompressedFileNames) <= 3.0.4-1
• rpmlib(FileDigests) <= 4.6.0-1
• rpmlib(PayloadFilesHavePrefix) <= 4.0-1
• rpmlib(PayloadIsZstd) <= 5.4.18-1
• rtld(GNU_HASH)

License

LGPL-2.1-only AND LGPL-2.1-only WITH OCaml-LGPL-linking-exception AND MIT AND BSD-3-Clause

Changelog

* Thu Jul 09 2026 Jerry James <loganjerry@gmail.com> - 9.2.0-2
  - OCaml 5.5.0 rebuild
  - Add patch to adapt to dune 3.24
  - Fix rocq.xml
* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 9.2.0-1
  - Version 9.2.0
  - Drop upstreamed documentation patch
  - Enable the native compiler for x86_64
* Fri Mar 20 2026 Jerry James <loganjerry@gmail.com> - 9.1.1-1
  - Initial RPM

Files

/usr/lib64/ocaml/coq
/usr/lib64/ocaml/coq/theories
/usr/lib64/ocaml/coq/theories/Array
/usr/lib64/ocaml/coq/theories/Array/.coq-native
/usr/lib64/ocaml/coq/theories/Array/.coq-native/NCorelib_Array_ArrayAxioms.cmi
/usr/lib64/ocaml/coq/theories/Array/.coq-native/NCorelib_Array_ArrayAxioms.cmxs
/usr/lib64/ocaml/coq/theories/Array/.coq-native/NCorelib_Array_PrimArray.cmi
/usr/lib64/ocaml/coq/theories/Array/.coq-native/NCorelib_Array_PrimArray.cmxs
/usr/lib64/ocaml/coq/theories/Array/ArrayAxioms.glob
/usr/lib64/ocaml/coq/theories/Array/ArrayAxioms.vo
/usr/lib64/ocaml/coq/theories/Array/PrimArray.glob
/usr/lib64/ocaml/coq/theories/Array/PrimArray.vo
/usr/lib64/ocaml/coq/theories/BinNums
/usr/lib64/ocaml/coq/theories/BinNums/.coq-native
/usr/lib64/ocaml/coq/theories/BinNums/.coq-native/NCorelib_BinNums_IntDef.cmi
/usr/lib64/ocaml/coq/theories/BinNums/.coq-native/NCorelib_BinNums_IntDef.cmxs
/usr/lib64/ocaml/coq/theories/BinNums/.coq-native/NCorelib_BinNums_NatDef.cmi
/usr/lib64/ocaml/coq/theories/BinNums/.coq-native/NCorelib_BinNums_NatDef.cmxs
/usr/lib64/ocaml/coq/theories/BinNums/.coq-native/NCorelib_BinNums_PosDef.cmi
/usr/lib64/ocaml/coq/theories/BinNums/.coq-native/NCorelib_BinNums_PosDef.cmxs
/usr/lib64/ocaml/coq/theories/BinNums/IntDef.glob
/usr/lib64/ocaml/coq/theories/BinNums/IntDef.vo
/usr/lib64/ocaml/coq/theories/BinNums/NatDef.glob
/usr/lib64/ocaml/coq/theories/BinNums/NatDef.vo
/usr/lib64/ocaml/coq/theories/BinNums/PosDef.glob
/usr/lib64/ocaml/coq/theories/BinNums/PosDef.vo
/usr/lib64/ocaml/coq/theories/Classes
/usr/lib64/ocaml/coq/theories/Classes/.coq-native
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_CMorphisms.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_CMorphisms.cmxs
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_CRelationClasses.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_CRelationClasses.cmxs
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Equivalence.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Equivalence.cmxs
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Init.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Init.cmxs
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms.cmxs
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms_Prop.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_Morphisms_Prop.cmxs
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_RelationClasses.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_RelationClasses.cmxs
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_SetoidTactics.cmi
/usr/lib64/ocaml/coq/theories/Classes/.coq-native/NCorelib_Classes_SetoidTactics.cmxs
/usr/lib64/ocaml/coq/theories/Classes/CMorphisms.glob
/usr/lib64/ocaml/coq/theories/Classes/CMorphisms.vo
/usr/lib64/ocaml/coq/theories/Classes/CRelationClasses.glob
/usr/lib64/ocaml/coq/theories/Classes/CRelationClasses.vo
/usr/lib64/ocaml/coq/theories/Classes/Equivalence.glob
/usr/lib64/ocaml/coq/theories/Classes/Equivalence.vo
/usr/lib64/ocaml/coq/theories/Classes/Init.glob
/usr/lib64/ocaml/coq/theories/Classes/Init.vo
/usr/lib64/ocaml/coq/theories/Classes/Morphisms.glob
/usr/lib64/ocaml/coq/theories/Classes/Morphisms.vo
/usr/lib64/ocaml/coq/theories/Classes/Morphisms_Prop.glob
/usr/lib64/ocaml/coq/theories/Classes/Morphisms_Prop.vo
/usr/lib64/ocaml/coq/theories/Classes/RelationClasses.glob
/usr/lib64/ocaml/coq/theories/Classes/RelationClasses.vo
/usr/lib64/ocaml/coq/theories/Classes/SetoidTactics.glob
/usr/lib64/ocaml/coq/theories/Classes/SetoidTactics.vo
/usr/lib64/ocaml/coq/theories/Compat
/usr/lib64/ocaml/coq/theories/Compat/.coq-native
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq818.cmi
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq818.cmxs
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq819.cmi
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq819.cmxs
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq820.cmi
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Coq820.cmxs
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Rocq90.cmi
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Rocq90.cmxs
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Rocq91.cmi
/usr/lib64/ocaml/coq/theories/Compat/.coq-native/NCorelib_Compat_Rocq91.cmxs
/usr/lib64/ocaml/coq/theories/Compat/Coq818.glob
/usr/lib64/ocaml/coq/theories/Compat/Coq818.vo
/usr/lib64/ocaml/coq/theories/Compat/Coq819.glob
/usr/lib64/ocaml/coq/theories/Compat/Coq819.vo
/usr/lib64/ocaml/coq/theories/Compat/Coq820.glob
/usr/lib64/ocaml/coq/theories/Compat/Coq820.vo
/usr/lib64/ocaml/coq/theories/Compat/Rocq90.glob
/usr/lib64/ocaml/coq/theories/Compat/Rocq90.vo
/usr/lib64/ocaml/coq/theories/Compat/Rocq91.glob
/usr/lib64/ocaml/coq/theories/Compat/Rocq91.vo
/usr/lib64/ocaml/coq/theories/Floats
/usr/lib64/ocaml/coq/theories/Floats/.coq-native
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatAxioms.cmi
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatAxioms.cmxs
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatClass.cmi
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatClass.cmxs
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatOps.cmi
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_FloatOps.cmxs
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_PrimFloat.cmi
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_PrimFloat.cmxs
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_SpecFloat.cmi
/usr/lib64/ocaml/coq/theories/Floats/.coq-native/NCorelib_Floats_SpecFloat.cmxs
/usr/lib64/ocaml/coq/theories/Floats/FloatAxioms.glob
/usr/lib64/ocaml/coq/theories/Floats/FloatAxioms.vo
/usr/lib64/ocaml/coq/theories/Floats/FloatClass.glob
/usr/lib64/ocaml/coq/theories/Floats/FloatClass.vo
/usr/lib64/ocaml/coq/theories/Floats/FloatOps.glob
/usr/lib64/ocaml/coq/theories/Floats/FloatOps.vo
/usr/lib64/ocaml/coq/theories/Floats/PrimFloat.glob
/usr/lib64/ocaml/coq/theories/Floats/PrimFloat.vo
/usr/lib64/ocaml/coq/theories/Floats/SpecFloat.glob
/usr/lib64/ocaml/coq/theories/Floats/SpecFloat.vo
/usr/lib64/ocaml/coq/theories/Init
/usr/lib64/ocaml/coq/theories/Init/.coq-native
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Byte.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Byte.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Datatypes.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Datatypes.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Decimal.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Decimal.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Equality.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Equality.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Hexadecimal.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Hexadecimal.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Logic.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Logic.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Ltac.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Ltac.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Nat.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Nat.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Notations.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Notations.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Number.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Number.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Peano.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Peano.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Prelude.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Prelude.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Specif.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Specif.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Sumbool.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Sumbool.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Tactics.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Tactics.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Tauto.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Tauto.cmxs
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Wf.cmi
/usr/lib64/ocaml/coq/theories/Init/.coq-native/NCorelib_Init_Wf.cmxs
/usr/lib64/ocaml/coq/theories/Init/Byte.glob
/usr/lib64/ocaml/coq/theories/Init/Byte.vo
/usr/lib64/ocaml/coq/theories/Init/Datatypes.glob
/usr/lib64/ocaml/coq/theories/Init/Datatypes.vo
/usr/lib64/ocaml/coq/theories/Init/Decimal.glob
/usr/lib64/ocaml/coq/theories/Init/Decimal.vo
/usr/lib64/ocaml/coq/theories/Init/Equality.glob
/usr/lib64/ocaml/coq/theories/Init/Equality.vo
/usr/lib64/ocaml/coq/theories/Init/Hexadecimal.glob
/usr/lib64/ocaml/coq/theories/Init/Hexadecimal.vo
/usr/lib64/ocaml/coq/theories/Init/Logic.glob
/usr/lib64/ocaml/coq/theories/Init/Logic.vo
/usr/lib64/ocaml/coq/theories/Init/Ltac.glob
/usr/lib64/ocaml/coq/theories/Init/Ltac.vo
/usr/lib64/ocaml/coq/theories/Init/Nat.glob
/usr/lib64/ocaml/coq/theories/Init/Nat.vo
/usr/lib64/ocaml/coq/theories/Init/Notations.glob
/usr/lib64/ocaml/coq/theories/Init/Notations.vo
/usr/lib64/ocaml/coq/theories/Init/Number.glob
/usr/lib64/ocaml/coq/theories/Init/Number.vo
/usr/lib64/ocaml/coq/theories/Init/Peano.glob
/usr/lib64/ocaml/coq/theories/Init/Peano.vo
/usr/lib64/ocaml/coq/theories/Init/Prelude.glob
/usr/lib64/ocaml/coq/theories/Init/Prelude.vo
/usr/lib64/ocaml/coq/theories/Init/Specif.glob
/usr/lib64/ocaml/coq/theories/Init/Specif.vo
/usr/lib64/ocaml/coq/theories/Init/Sumbool.glob
/usr/lib64/ocaml/coq/theories/Init/Sumbool.vo
/usr/lib64/ocaml/coq/theories/Init/Tactics.glob
/usr/lib64/ocaml/coq/theories/Init/Tactics.vo
/usr/lib64/ocaml/coq/theories/Init/Tauto.glob
/usr/lib64/ocaml/coq/theories/Init/Tauto.vo
/usr/lib64/ocaml/coq/theories/Init/Wf.glob
/usr/lib64/ocaml/coq/theories/Init/Wf.vo
/usr/lib64/ocaml/coq/theories/Lists
/usr/lib64/ocaml/coq/theories/Lists/.coq-native
/usr/lib64/ocaml/coq/theories/Lists/.coq-native/NCorelib_Lists_ListDef.cmi
/usr/lib64/ocaml/coq/theories/Lists/.coq-native/NCorelib_Lists_ListDef.cmxs
/usr/lib64/ocaml/coq/theories/Lists/ListDef.glob
/usr/lib64/ocaml/coq/theories/Lists/ListDef.vo
/usr/lib64/ocaml/coq/theories/Numbers
/usr/lib64/ocaml/coq/theories/Numbers/.coq-native
/usr/lib64/ocaml/coq/theories/Numbers/.coq-native/NCorelib_Numbers_BinNums.cmi
/usr/lib64/ocaml/coq/theories/Numbers/.coq-native/NCorelib_Numbers_BinNums.cmxs
/usr/lib64/ocaml/coq/theories/Numbers/BinNums.glob
/usr/lib64/ocaml/coq/theories/Numbers/BinNums.vo
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_CarryType.cmi
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_CarryType.cmxs
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_PrimInt63.cmi
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_PrimInt63.cmxs
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Sint63Axioms.cmi
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Sint63Axioms.cmxs
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Uint63Axioms.cmi
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCorelib_Numbers_Cyclic_Int63_Uint63Axioms.cmxs
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/CarryType.glob
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/CarryType.v
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/CarryType.vo
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/PrimInt63.glob
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/PrimInt63.v
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/PrimInt63.vo
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.glob
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.v
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.vo
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.glob
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.v
/usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.vo
/usr/lib64/ocaml/coq/theories/Program
/usr/lib64/ocaml/coq/theories/Program/.coq-native
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Basics.cmi
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Basics.cmxs
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Tactics.cmi
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Tactics.cmxs
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Utils.cmi
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Utils.cmxs
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Wf.cmi
/usr/lib64/ocaml/coq/theories/Program/.coq-native/NCorelib_Program_Wf.cmxs
/usr/lib64/ocaml/coq/theories/Program/Basics.glob
/usr/lib64/ocaml/coq/theories/Program/Basics.vo
/usr/lib64/ocaml/coq/theories/Program/Tactics.glob
/usr/lib64/ocaml/coq/theories/Program/Tactics.vo
/usr/lib64/ocaml/coq/theories/Program/Utils.glob
/usr/lib64/ocaml/coq/theories/Program/Utils.vo
/usr/lib64/ocaml/coq/theories/Program/Wf.glob
/usr/lib64/ocaml/coq/theories/Program/Wf.vo
/usr/lib64/ocaml/coq/theories/Relations
/usr/lib64/ocaml/coq/theories/Relations/.coq-native
/usr/lib64/ocaml/coq/theories/Relations/.coq-native/NCorelib_Relations_Relation_Definitions.cmi
/usr/lib64/ocaml/coq/theories/Relations/.coq-native/NCorelib_Relations_Relation_Definitions.cmxs
/usr/lib64/ocaml/coq/theories/Relations/Relation_Definitions.glob
/usr/lib64/ocaml/coq/theories/Relations/Relation_Definitions.vo
/usr/lib64/ocaml/coq/theories/Setoids
/usr/lib64/ocaml/coq/theories/Setoids/.coq-native
/usr/lib64/ocaml/coq/theories/Setoids/.coq-native/NCorelib_Setoids_Setoid.cmi
/usr/lib64/ocaml/coq/theories/Setoids/.coq-native/NCorelib_Setoids_Setoid.cmxs
/usr/lib64/ocaml/coq/theories/Setoids/Setoid.glob
/usr/lib64/ocaml/coq/theories/Setoids/Setoid.vo
/usr/lib64/ocaml/coq/theories/Strings
/usr/lib64/ocaml/coq/theories/Strings/.coq-native
/usr/lib64/ocaml/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimString.cmi
/usr/lib64/ocaml/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimString.cmxs
/usr/lib64/ocaml/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimStringAxioms.cmi
/usr/lib64/ocaml/coq/theories/Strings/.coq-native/NCorelib_Strings_PrimStringAxioms.cmxs
/usr/lib64/ocaml/coq/theories/Strings/PrimString.glob
/usr/lib64/ocaml/coq/theories/Strings/PrimString.vo
/usr/lib64/ocaml/coq/theories/Strings/PrimStringAxioms.glob
/usr/lib64/ocaml/coq/theories/Strings/PrimStringAxioms.vo
/usr/lib64/ocaml/coq/theories/derive
/usr/lib64/ocaml/coq/theories/derive/.coq-native
/usr/lib64/ocaml/coq/theories/derive/.coq-native/NCorelib_derive_Derive.cmi
/usr/lib64/ocaml/coq/theories/derive/.coq-native/NCorelib_derive_Derive.cmxs
/usr/lib64/ocaml/coq/theories/derive/Derive.glob
/usr/lib64/ocaml/coq/theories/derive/Derive.vo
/usr/lib64/ocaml/coq/theories/extraction
/usr/lib64/ocaml/coq/theories/extraction/.coq-native
/usr/lib64/ocaml/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrHaskellBasic.cmi
/usr/lib64/ocaml/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrHaskellBasic.cmxs
/usr/lib64/ocaml/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrOcamlBasic.cmi
/usr/lib64/ocaml/coq/theories/extraction/.coq-native/NCorelib_extraction_ExtrOcamlBasic.cmxs
/usr/lib64/ocaml/coq/theories/extraction/.coq-native/NCorelib_extraction_Extraction.cmi
/usr/lib64/ocaml/coq/theories/extraction/.coq-native/NCorelib_extraction_Extraction.cmxs
/usr/lib64/ocaml/coq/theories/extraction/ExtrHaskellBasic.glob
/usr/lib64/ocaml/coq/theories/extraction/ExtrHaskellBasic.vo
/usr/lib64/ocaml/coq/theories/extraction/ExtrOcamlBasic.glob
/usr/lib64/ocaml/coq/theories/extraction/ExtrOcamlBasic.vo
/usr/lib64/ocaml/coq/theories/extraction/Extraction.glob
/usr/lib64/ocaml/coq/theories/extraction/Extraction.vo
/usr/lib64/ocaml/coq/theories/ssr
/usr/lib64/ocaml/coq/theories/ssr/.coq-native
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrbool.cmi
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrbool.cmxs
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrclasses.cmi
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrclasses.cmxs
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssreflect.cmi
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssreflect.cmxs
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrfun.cmi
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrfun.cmxs
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrsetoid.cmi
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrsetoid.cmxs
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrunder.cmi
/usr/lib64/ocaml/coq/theories/ssr/.coq-native/NCorelib_ssr_ssrunder.cmxs
/usr/lib64/ocaml/coq/theories/ssr/ssrbool.glob
/usr/lib64/ocaml/coq/theories/ssr/ssrbool.vo
/usr/lib64/ocaml/coq/theories/ssr/ssrclasses.glob
/usr/lib64/ocaml/coq/theories/ssr/ssrclasses.vo
/usr/lib64/ocaml/coq/theories/ssr/ssreflect.glob
/usr/lib64/ocaml/coq/theories/ssr/ssreflect.vo
/usr/lib64/ocaml/coq/theories/ssr/ssrfun.glob
/usr/lib64/ocaml/coq/theories/ssr/ssrfun.vo
/usr/lib64/ocaml/coq/theories/ssr/ssrsetoid.glob
/usr/lib64/ocaml/coq/theories/ssr/ssrsetoid.vo
/usr/lib64/ocaml/coq/theories/ssr/ssrunder.glob
/usr/lib64/ocaml/coq/theories/ssr/ssrunder.vo
/usr/lib64/ocaml/coq/theories/ssrmatching
/usr/lib64/ocaml/coq/theories/ssrmatching/.coq-native
/usr/lib64/ocaml/coq/theories/ssrmatching/.coq-native/NCorelib_ssrmatching_ssrmatching.cmi
/usr/lib64/ocaml/coq/theories/ssrmatching/.coq-native/NCorelib_ssrmatching_ssrmatching.cmxs
/usr/lib64/ocaml/coq/theories/ssrmatching/ssrmatching.glob
/usr/lib64/ocaml/coq/theories/ssrmatching/ssrmatching.vo
/usr/lib64/ocaml/coq/user-contrib
/usr/lib64/ocaml/coq/user-contrib/Ltac2
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constant.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constant.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constructor.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constructor.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Evar.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Evar.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_FMap.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_FMap.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_FSet.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_FSet.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Float.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Float.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ind.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ind.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Lazy.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Lazy.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1CompatNotations.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1CompatNotations.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Meta.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Meta.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Module.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Module.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Printf.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Printf.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Proj.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Proj.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pstring.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pstring.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_RedFlags.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_RedFlags.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ref.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ref.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Reference.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Reference.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Rewrite.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Rewrite.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_TransparentState.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_TransparentState.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Uint63.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Uint63.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Unification.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Unification.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Array.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Array.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Array.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Bool.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Bool.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Bool.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Char.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Char.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Char.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/.coq-native
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq818.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq818.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq819.cmi
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq819.cmxs
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq818.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq818.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq819.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq819.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constant.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constant.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constant.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constr.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constr.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constr.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constructor.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constructor.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Constructor.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Control.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Control.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Control.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Env.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Env.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Env.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Evar.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Evar.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Evar.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/FMap.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/FMap.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/FMap.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/FSet.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/FSet.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/FSet.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Float.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Float.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Float.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Fresh.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Fresh.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Fresh.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ident.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ident.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ident.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ind.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ind.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ind.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Init.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Init.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Init.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Int.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Int.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Int.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Lazy.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Lazy.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Lazy.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/List.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/List.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/List.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1CompatNotations.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1CompatNotations.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1CompatNotations.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac2.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac2.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac2.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Message.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Message.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Message.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Meta.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Meta.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Meta.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Module.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Module.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Module.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Notations.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Notations.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Notations.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Option.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Option.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Option.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Pattern.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Pattern.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Pattern.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Printf.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Printf.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Printf.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Proj.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Proj.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Proj.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Pstring.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Pstring.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Pstring.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/RedFlags.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/RedFlags.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/RedFlags.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ref.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ref.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Ref.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Reference.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Reference.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Reference.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Rewrite.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Rewrite.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Rewrite.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Std.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Std.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Std.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/String.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/String.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/String.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/TransparentState.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/TransparentState.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/TransparentState.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Uint63.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Uint63.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Uint63.vo
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Unification.glob
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Unification.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Unification.vo
/usr/lib64/ocaml/rocq-core
/usr/lib64/ocaml/rocq-core/META
/usr/lib64/ocaml/rocq-core/dune-package
/usr/lib64/ocaml/rocq-core/opam

Generated by rpm2html 1.8.1

Fabrice Bellet, Mon Jul 20 22:21:06 2026