rocq-core-source-9.1.1-1.fc44 RPM for ppc64le

From Fedora 44 testing updates for ppc64le / Packages / 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 contains the source Rocq files for the Rocq Prelude, and the
Corelib and Ltac2 modules.  These files are not needed to use the Rocq Prelude,
and the Corelib and Ltac2 modules.  They are made available for informational
purposes.

Provides

• rocq-core-source
• rocq-core-source(ppc-64)

Requires

• rocq-core(ppc-64) = 9.1.1-1.fc44
• rpmlib(CompressedFileNames) <= 3.0.4-1
• rpmlib(FileDigests) <= 4.6.0-1
• rpmlib(PayloadFilesHavePrefix) <= 4.0-1
• rpmlib(PayloadIsZstd) <= 5.4.18-1

License

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

Changelog

* Fri Mar 20 2026 Jerry James <loganjerry@gmail.com> - 9.1.1-1
  - Initial RPM

Files

/usr/lib64/ocaml/coq/theories/Array/ArrayAxioms.v
/usr/lib64/ocaml/coq/theories/Array/PrimArray.v
/usr/lib64/ocaml/coq/theories/BinNums/IntDef.v
/usr/lib64/ocaml/coq/theories/BinNums/NatDef.v
/usr/lib64/ocaml/coq/theories/BinNums/PosDef.v
/usr/lib64/ocaml/coq/theories/Classes/CMorphisms.v
/usr/lib64/ocaml/coq/theories/Classes/CRelationClasses.v
/usr/lib64/ocaml/coq/theories/Classes/Equivalence.v
/usr/lib64/ocaml/coq/theories/Classes/Init.v
/usr/lib64/ocaml/coq/theories/Classes/Morphisms.v
/usr/lib64/ocaml/coq/theories/Classes/Morphisms_Prop.v
/usr/lib64/ocaml/coq/theories/Classes/RelationClasses.v
/usr/lib64/ocaml/coq/theories/Classes/SetoidTactics.v
/usr/lib64/ocaml/coq/theories/Compat/Coq818.v
/usr/lib64/ocaml/coq/theories/Compat/Coq819.v
/usr/lib64/ocaml/coq/theories/Compat/Coq820.v
/usr/lib64/ocaml/coq/theories/Compat/Rocq90.v
/usr/lib64/ocaml/coq/theories/Floats/FloatAxioms.v
/usr/lib64/ocaml/coq/theories/Floats/FloatClass.v
/usr/lib64/ocaml/coq/theories/Floats/FloatOps.v
/usr/lib64/ocaml/coq/theories/Floats/PrimFloat.v
/usr/lib64/ocaml/coq/theories/Floats/SpecFloat.v
/usr/lib64/ocaml/coq/theories/Init/Byte.v
/usr/lib64/ocaml/coq/theories/Init/Datatypes.v
/usr/lib64/ocaml/coq/theories/Init/Decimal.v
/usr/lib64/ocaml/coq/theories/Init/Hexadecimal.v
/usr/lib64/ocaml/coq/theories/Init/Logic.v
/usr/lib64/ocaml/coq/theories/Init/Ltac.v
/usr/lib64/ocaml/coq/theories/Init/Nat.v
/usr/lib64/ocaml/coq/theories/Init/Notations.v
/usr/lib64/ocaml/coq/theories/Init/Number.v
/usr/lib64/ocaml/coq/theories/Init/Peano.v
/usr/lib64/ocaml/coq/theories/Init/Prelude.v
/usr/lib64/ocaml/coq/theories/Init/Specif.v
/usr/lib64/ocaml/coq/theories/Init/Sumbool.v
/usr/lib64/ocaml/coq/theories/Init/Tactics.v
/usr/lib64/ocaml/coq/theories/Init/Tauto.v
/usr/lib64/ocaml/coq/theories/Init/Wf.v
/usr/lib64/ocaml/coq/theories/Lists/ListDef.v
/usr/lib64/ocaml/coq/theories/Numbers/BinNums.v
/usr/lib64/ocaml/coq/theories/Program/Basics.v
/usr/lib64/ocaml/coq/theories/Program/Tactics.v
/usr/lib64/ocaml/coq/theories/Program/Utils.v
/usr/lib64/ocaml/coq/theories/Program/Wf.v
/usr/lib64/ocaml/coq/theories/Relations/Relation_Definitions.v
/usr/lib64/ocaml/coq/theories/Setoids/Setoid.v
/usr/lib64/ocaml/coq/theories/Strings/PrimString.v
/usr/lib64/ocaml/coq/theories/Strings/PrimStringAxioms.v
/usr/lib64/ocaml/coq/theories/derive/Derive.v
/usr/lib64/ocaml/coq/theories/extraction/ExtrHaskellBasic.v
/usr/lib64/ocaml/coq/theories/extraction/ExtrOcamlBasic.v
/usr/lib64/ocaml/coq/theories/extraction/Extraction.v
/usr/lib64/ocaml/coq/theories/ssr/ssrbool.v
/usr/lib64/ocaml/coq/theories/ssr/ssrclasses.v
/usr/lib64/ocaml/coq/theories/ssr/ssreflect.v
/usr/lib64/ocaml/coq/theories/ssr/ssrfun.v
/usr/lib64/ocaml/coq/theories/ssr/ssrsetoid.v
/usr/lib64/ocaml/coq/theories/ssr/ssrunder.v
/usr/lib64/ocaml/coq/theories/ssrmatching/ssrmatching.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq818.v
/usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq819.v

Generated by rpm2html 1.8.1

Fabrice Bellet, Sat Apr 18 01:39:05 2026