Index index by Group index by Distribution index by Vendor index by creation date index by Name Mirrors Help Search

rocq-core-source-9.2.0-1.fc45 RPM for aarch64

From Fedora Rawhide for aarch64 / r

Name: rocq-core-source Distribution: Fedora Project
Version: 9.2.0 Vendor: Fedora Project
Release: 1.fc45 Build date: Thu Apr 16 18:24:43 2026
Group: Unspecified Build host: buildvm-a64-15.rdu3.fedoraproject.org
Size: 575383 Source RPM: rocq-9.2.0-1.fc45.src.rpm
Packager: Fedora Project
Url: https://rocq-prover.org/
Summary: Source files of the Rocq Prelude, and the Corelib and Ltac2 modules
 
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

Requires

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/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/Compat/Rocq91.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/Equality.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, Fri May 15 23:13:04 2026