rocq-core-9.2.0-1.fc45 RPM for ppc64le

From Fedora Rawhide for ppc64le / 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
• rocq-core(ppc-64)

Requires

• rocq-runtime(ppc-64) = 9.2.0-1.fc45
• 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

* 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/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/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/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/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/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/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/ListDef.glob
/usr/lib64/ocaml/coq/theories/Lists/ListDef.vo
/usr/lib64/ocaml/coq/theories/Numbers
/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/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/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/Relation_Definitions.glob
/usr/lib64/ocaml/coq/theories/Relations/Relation_Definitions.vo
/usr/lib64/ocaml/coq/theories/Setoids
/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/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/Derive.glob
/usr/lib64/ocaml/coq/theories/derive/Derive.vo
/usr/lib64/ocaml/coq/theories/extraction
/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/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/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/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/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, Wed May 13 00:49:32 2026