rocq-stdlib-source-9.1.0-4.fc45 in Fedora Rawhide
↵ Return to the main page of rocq-stdlib-source
View build
Search for updates
Package Info (Data from x86_64 build)
🠗 Changelog
🠗 Dependencies
🠗 Provides
🠗 Files
Changelog
| Date | Author | Change |
|---|---|---|
| 2026-07-16 | Fedora Release Engineering <releng at fedoraproject dot org> - 9.1.0-4 | - Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild |
| 2026-07-09 | Jerry James <loganjerry at gmail dot com> - 9.1.0-3 | - OCaml 5.5.0 rebuild - Use the dune declarative buildsystem - Add patch for dune 3.24 compatibility |
| 2026-04-16 | Jerry James <loganjerry at gmail dot com> - 9.1.0-2 | - Rebuild for rocq 9.2.0 |
| 2026-03-20 | Jerry James <loganjerry at gmail dot com> - 9.1.0-1 | - Initial RPM |
Dependencies
- rocq-stdlib = 9.1.0-4.fc45
Provides
- rocq-stdlib-source
- rocq-stdlib-source(x86-64)
Files
- usr/
- lib64/
- ocaml/
- coq/
- user-contrib/
- Stdlib/
- All.v
- Arith/
- Arith.v
- Arith_base.v
- Between.v
- Bool_nat.v
- Cantor.v
- Compare.v
- Compare_dec.v
- EqNat.v
- Euclid.v
- Factorial.v
- PeanoNat.v
- Peano_dec.v
- Wf_nat.v
- Zerob.v
- Array/
- ArrayAxioms.v
- PArray.v
- PrimArray.v
- BinNums/
- IntDef.v
- NatDef.v
- PosDef.v
- Bool/
- Bool.v
- BoolEq.v
- DecBool.v
- IfProp.v
- Classes/
- CEquivalence.v
- CMorphisms.v
- CRelationClasses.v
- DecidableClass.v
- EquivDec.v
- Equivalence.v
- Init.v
- Morphisms.v
- Morphisms_Prop.v
- Morphisms_Relations.v
- RelationClasses.v
- RelationPairs.v
- SetoidClass.v
- SetoidDec.v
- SetoidTactics.v
- Compat/
- AdmitAxiom.v
- Coq818.v
- Coq819.v
- Coq820.v
- Stdlib818.v
- FSets/
- FMapAVL.v
- FMapFacts.v
- FMapFullAVL.v
- FMapInterface.v
- FMapList.v
- FMapPositive.v
- FMapWeakList.v
- FMaps.v
- FSetAVL.v
- FSetBridge.v
- FSetCompat.v
- FSetDecide.v
- FSetEqProperties.v
- FSetFacts.v
- FSetInterface.v
- FSetList.v
- FSetPositive.v
- FSetProperties.v
- FSetToFiniteSet.v
- FSetWeakList.v
- FSets.v
- Floats/
- FloatAxioms.v
- FloatClass.v
- FloatLemmas.v
- FloatOps.v
- Floats.v
- PrimFloat.v
- SpecFloat.v
- Init/
- Byte.v
- Datatypes.v
- Decimal.v
- Hexadecimal.v
- Logic.v
- Ltac.v
- Nat.v
- Notations.v
- Number.v
- Peano.v
- Prelude.v
- Specif.v
- Sumbool.v
- Tactics.v
- Tauto.v
- Wf.v
- Lists/
- Finite.v
- List.v
- ListDec.v
- ListDef.v
- ListSet.v
- ListTactics.v
- Logic/
- Adjointification.v
- Berardi.v
- ChoiceFacts.v
- Classical.v
- ClassicalChoice.v
- ClassicalDescription.v
- ClassicalEpsilon.v
- ClassicalFacts.v
- ClassicalUniqueChoice.v
- Classical_Pred_Type.v
- Classical_Prop.v
- ConstructiveEpsilon.v
- Decidable.v
- Description.v
- Diaconescu.v
- Epsilon.v
- Eqdep.v
- EqdepFacts.v
- Eqdep_dec.v
- ExtensionalFunctionRepresentative.v
- ExtensionalityFacts.v
- FunctionalExtensionality.v
- HLevels.v
- HLevelsBase.v
- Hurkens.v
- IndefiniteDescription.v
- JMeq.v
- ProofIrrelevance.v
- ProofIrrelevanceFacts.v
- PropExtensionality.v
- PropExtensionalityFacts.v
- PropFacts.v
- RelationalChoice.v
- SetIsType.v
- SetoidChoice.v
- StrictProp.v
- WKL.v
- WeakFan.v
- MSets/
- MSetAVL.v
- MSetDecide.v
- MSetEqProperties.v
- MSetFacts.v
- MSetGenTree.v
- MSetInterface.v
- MSetList.v
- MSetPositive.v
- MSetProperties.v
- MSetRBT.v
- MSetToFiniteSet.v
- MSetWeakList.v
- MSets.v
- NArith/
- BinNat.v
- BinNatDef.v
- NArith.v
- NArith_base.v
- Ndec.v
- Ndiv_def.v
- Ngcd_def.v
- Nnat.v
- Nsqrt_def.v
- Numbers/
- AltBinNotations.v
- BinNums.v
- Cyclic/
- Abstract/
- CyclicAxioms.v
- DoubleType.v
- NZCyclic.v
- Int63/
- CarryType.v
- Cyclic63.v
- PrimInt63.v
- Ring63.v
- Sint63.v
- Sint63Axioms.v
- Uint63.v
- Uint63Axioms.v
- Abstract/
- DecimalFacts.v
- DecimalN.v
- DecimalNat.v
- DecimalPos.v
- DecimalQ.v
- DecimalR.v
- DecimalString.v
- DecimalZ.v
- HexadecimalFacts.v
- HexadecimalN.v
- HexadecimalNat.v
- HexadecimalPos.v
- HexadecimalQ.v
- HexadecimalR.v
- HexadecimalString.v
- HexadecimalZ.v
- Integer/
- Abstract/
- ZAdd.v
- ZAddOrder.v
- ZAxioms.v
- ZBase.v
- ZBits.v
- ZDivEucl.v
- ZDivFloor.v
- ZDivTrunc.v
- ZGcd.v
- ZLcm.v
- ZLt.v
- ZMaxMin.v
- ZMul.v
- ZMulOrder.v
- ZParity.v
- ZPow.v
- ZProperties.v
- ZSgnAbs.v
- Binary/
- ZBinary.v
- NatPairs/
- ZNatPairs.v
- Abstract/
- NaryFunctions.v
- NatInt/
- NZAdd.v
- NZAddOrder.v
- NZAxioms.v
- NZBase.v
- NZBits.v
- NZDiv.v
- NZDomain.v
- NZGcd.v
- NZLog.v
- NZMul.v
- NZMulOrder.v
- NZOrder.v
- NZParity.v
- NZPow.v
- NZProperties.v
- NZSqrt.v
- Natural/
- Abstract/
- NAdd.v
- NAddOrder.v
- NAxioms.v
- NBase.v
- NBits.v
- NDefOps.v
- NDiv.v
- NDiv0.v
- NGcd.v
- NIso.v
- NLcm.v
- NLcm0.v
- NLog.v
- NMaxMin.v
- NMulOrder.v
- NOrder.v
- NParity.v
- NPow.v
- NProperties.v
- NSqrt.v
- NStrongRec.v
- NSub.v
- Binary/
- NBinary.v
- Abstract/
- NumPrelude.v
- PArith/
- BinPos.v
- BinPosDef.v
- PArith.v
- POrderedType.v
- Pnat.v
- Program/
- Basics.v
- Combinators.v
- Equality.v
- Program.v
- Subset.v
- Syntax.v
- Tactics.v
- Utils.v
- Wf.v
- WfExtensionality.v
- QArith/
- QArith.v
- QArith_base.v
- QNsatz.v
- QOrderedType.v
- Qabs.v
- Qcabs.v
- Qcanon.v
- Qfield.v
- Qminmax.v
- Qpower.v
- Qreduction.v
- Qring.v
- Qround.v
- Reals/
- Abstract/
- ConstructiveAbs.v
- ConstructiveLUB.v
- ConstructiveLimits.v
- ConstructiveMinMax.v
- ConstructivePower.v
- ConstructiveReals.v
- ConstructiveRealsMorphisms.v
- ConstructiveSum.v
- Alembert.v
- AltSeries.v
- ArithProp.v
- Binomial.v
- Cauchy/
- ConstructiveCauchyAbs.v
- ConstructiveCauchyReals.v
- ConstructiveCauchyRealsMult.v
- ConstructiveExtra.v
- ConstructiveRcomplete.v
- PosExtra.v
- QExtra.v
- Cauchy_prod.v
- ClassicalConstructiveReals.v
- ClassicalDedekindReals.v
- Cos_plus.v
- Cos_rel.v
- DiscrR.v
- Exp_prop.v
- Integration.v
- MVT.v
- Machin.v
- NewtonInt.v
- Nsatz.v
- PSeries_reg.v
- PartSum.v
- Qreals.v
- RIneq.v
- RList.v
- RNsatz.v
- ROrderedType.v
- R_Ifp.v
- R_sqr.v
- R_sqrt.v
- Ranalysis.v
- Ranalysis1.v
- Ranalysis2.v
- Ranalysis3.v
- Ranalysis4.v
- Ranalysis5.v
- Ranalysis_reg.v
- Ratan.v
- Raxioms.v
- Rbase.v
- Rbasic_fun.v
- Rcomplete.v
- Rdefinitions.v
- Rderiv.v
- Reals.v
- Rfunctions.v
- Rgeom.v
- RiemannInt.v
- RiemannInt_SF.v
- Rlimit.v
- Rlogic.v
- Rminmax.v
- Rpow_def.v
- Rpower.v
- Rprod.v
- Rregisternames.v
- Rseries.v
- Rsigma.v
- Rsqrt_def.v
- Rtopology.v
- Rtrigo.v
- Rtrigo1.v
- Rtrigo_alt.v
- Rtrigo_calc.v
- Rtrigo_def.v
- Rtrigo_facts.v
- Rtrigo_fun.v
- Rtrigo_reg.v
- Runcountable.v
- SeqProp.v
- SeqSeries.v
- SplitAbsolu.v
- SplitRmult.v
- Sqrt_reg.v
- Zfloor.v
- Abstract/
- Relations/
- Operators_Properties.v
- Relation_Definitions.v
- Relation_Operators.v
- Relations.v
- Setoids/
- Setoid.v
- Sets/
- Classical_sets.v
- Constructive_sets.v
- Cpo.v
- Ensembles.v
- Finite_sets.v
- Finite_sets_facts.v
- Image.v
- Infinite_sets.v
- Integers.v
- Multiset.v
- Partial_Order.v
- Permut.v
- Powerset.v
- Powerset_Classical_facts.v
- Powerset_facts.v
- Relations_1.v
- Relations_1_facts.v
- Relations_2.v
- Relations_2_facts.v
- Relations_3.v
- Relations_3_facts.v
- Uniset.v
- Sorting/
- CPermutation.v
- Heap.v
- Mergesort.v
- PermutEq.v
- PermutSetoid.v
- Permutation.v
- SetoidList.v
- SetoidPermutation.v
- Sorted.v
- Sorting.v
- Streams/
- StreamMemo.v
- Streams.v
- Strings/
- Ascii.v
- BinaryString.v
- Byte.v
- HexString.v
- OctalString.v
- PString.v
- PrimString.v
- PrimStringAxioms.v
- String.v
- Structures/
- BoolOrder.v
- DecidableType.v
- DecidableTypeEx.v
- Equalities.v
- EqualitiesFacts.v
- GenericMinMax.v
- OrderedType.v
- OrderedTypeAlt.v
- OrderedTypeEx.v
- Orders.v
- OrdersAlt.v
- OrdersEx.v
- OrdersFacts.v
- OrdersLists.v
- OrdersTac.v
- Unicode/
- Utf8.v
- Utf8_core.v
- Vectors/
- Bvector.v
- Fin.v
- FinFun.v
- Vector.v
- VectorDef.v
- VectorEq.v
- VectorSpec.v
- Wellfounded/
- Disjoint_Union.v
- Inclusion.v
- Inverse_Image.v
- Lexicographic_Exponentiation.v
- Lexicographic_Product.v
- List_Extension.v
- Transitive_Closure.v
- Union.v
- Well_Ordering.v
- Wellfounded.v
- ZArith/
- BinInt.v
- BinIntDef.v
- Int.v
- Wf_Z.v
- ZArith.v
- ZArith_base.v
- ZArith_dec.v
- ZModOffset.v
- ZNsatz.v
- Zabs.v
- Zbitwise.v
- Zbool.v
- Zcompare.v
- Zcomplements.v
- Zcong.v
- Zdiv.v
- Zdiv_facts.v
- Zdivisibility.v
- Zeuclid.v
- Zeven.v
- Zgcd_alt.v
- Zhints.v
- Zmax.v
- Zmin.v
- Zminmax.v
- Zmisc.v
- Znat.v
- Znumtheory.v
- Zorder.v
- Zpow_alt.v
- Zpow_def.v
- Zpow_facts.v
- Zpower.v
- Zquot.v
- Zwf.v
- auxiliary.v
- Zmod/
- Bits.v
- Zmod.v
- ZmodBase.v
- ZmodDef.v
- ZmodInv.v
- ZmodNsatz.v
- Zstar.v
- ZstarBase.v
- ZstarDef.v
- btauto/
- Algebra.v
- Btauto.v
- Reflect.v
- derive/
- Derive.v
- extraction/
- ExtrHaskellBasic.v
- ExtrHaskellNatInt.v
- ExtrHaskellNatInteger.v
- ExtrHaskellNatNum.v
- ExtrHaskellString.v
- ExtrHaskellZInt.v
- ExtrHaskellZInteger.v
- ExtrHaskellZNum.v
- ExtrOCamlFloats.v
- ExtrOCamlInt63.v
- ExtrOCamlPArray.v
- ExtrOCamlPString.v
- ExtrOcamlBasic.v
- ExtrOcamlChar.v
- ExtrOcamlIntConv.v
- ExtrOcamlNatBigInt.v
- ExtrOcamlNatInt.v
- ExtrOcamlNativeString.v
- ExtrOcamlString.v
- ExtrOcamlZBigInt.v
- ExtrOcamlZInt.v
- Extraction.v
- funind/
- FunInd.v
- Recdef.v
- micromega/
- DeclConstant.v
- DeclConstantZ.v
- Env.v
- EnvRing.v
- Fourier.v
- Fourier_util.v
- Lia.v
- Lqa.v
- Lra.v
- OrderedRing.v
- Psatz.v
- QMicromega.v
- RMicromega.v
- Refl.v
- RingMicromega.v
- SatDivMod.v
- Tauto.v
- VarMap.v
- ZArith_hints.v
- ZCoeff.v
- ZMicromega.v
- Zify.v
- ZifyBool.v
- ZifyClasses.v
- ZifyComparison.v
- ZifyInst.v
- ZifyN.v
- ZifyNat.v
- ZifyPow.v
- ZifySint63.v
- ZifyUint63.v
- Ztac.v
- nsatz/
- ENsatzTactic.v
- NsatzTactic.v
- omega/
- OmegaLemmas.v
- PreOmega.v
- rtauto/
- Bintree.v
- Rtauto.v
- setoid_ring/
- Algebra_syntax.v
- ArithRing.v
- BinList.v
- Cring.v
- Field.v
- Field_tac.v
- Field_theory.v
- InitialRing.v
- Integral_domain.v
- NArithRing.v
- Ncring.v
- Ncring_initial.v
- Ncring_polynom.v
- Ncring_tac.v
- RealField.v
- Ring.v
- Ring_base.v
- Ring_polynom.v
- Ring_tac.v
- Ring_theory.v
- Rings_Q.v
- Rings_R.v
- Rings_Z.v
- ZArithRing.v
- ssr/
- ssrbool.v
- ssrclasses.v
- ssreflect.v
- ssrfun.v
- ssrsetoid.v
- ssrunder.v
- ssrmatching/
- ssrmatching.v
- Stdlib/
- user-contrib/
- coq/
- ocaml/
- lib64/
Sources on Pagure