SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

gappalib-coq rpm build for : Fedora 39. For other distributions click gappalib-coq.

Name : gappalib-coq
Version : 1.5.3 Vendor : Fedora Project
Release : 4.fc39 Date : 2023-07-27 19:33:04
Group : Unspecified Source RPM : gappalib-coq-1.5.3-4.fc39.src.rpm
Size : 2.25 MB
Packager : Fedora Project
Summary : Coq support library for gappa
Description :
This support library provides vernacular files so that the certificates
Gappa generates can be imported by the Coq proof assistant. It also
provides a \"gappa\" tactic that calls Gappa on the current Coq goal.

Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques --
automatic proof generation of arithmetic properties) is a tool intended
to help verifying and formally proving properties on numerical programs
dealing with floating-point or fixed-point arithmetic.

RPM found in directory: /vol/rzm3/linux-fedora-buffet/fedora/linux/releases/39/Everything/x86_64/os/Packages/g

Content of RPM  Changelog  Provides Requires

Download
ftp.icm.edu.pl  gappalib-coq-1.5.3-4.fc39.x86_64.rpm
     

Provides :
gappalib-coq
gappalib-coq(x86-64)
ocaml(Gappatac)

Requires :
coq(x86-64) = 8.17.1
flocq
gappa
ocaml(AcyclicGraph) = 075502ca3357cf235179ed6b9b34d699
ocaml(Attributes) = 10a9271295c73222723c35d497a9c142
ocaml(Big_int_Z) = 981a14e500660f2c264fb221a4e70905
ocaml(CArray) = 6d58569e3639e38decf1a0dbacbf0726
ocaml(CAst) = 42d6ecfe3ce9d100a355b5990a884114
ocaml(CClosure) = e6f92f47a3a34da19529eb5ab292a15c
ocaml(CDebug) = 326079a49c3f190b8b7ab5844c584942
ocaml(CEphemeron) = 93e20cd55896e94be0d04b06c6571279
ocaml(CErrors) = 00917bcf8ba9a78b4ea100f83590b566
ocaml(CList) = f40080596f5cf76bf47880b35de4d520
ocaml(CMap) = 57c0f678ba0c1d7497fe55560bcebe5e
ocaml(CPrimitives) = ee0d0284977cedc9a396190afc96b017
ocaml(CSet) = 7d7be9cc23fb38e10753233bf859750e
ocaml(CSig) = cbe0b0a079f2ef2dcd13f42ae80840dd
ocaml(CString) = a4fefb8c8cd7dd8cf22cbb31ad12719e
ocaml(CUnix) = 02c1e8f824a500e558673c6fa375775f
ocaml(CamlinternalFormatBasics) = cecfafd5c021473f5e358c96ac7502a0
ocaml(CamlinternalLazy) = 2c797917c31a980b79e9d16d84057b70
ocaml(Coercionops) = 72d5956fe74aa7305ae3bbb641e3b983
ocaml(Constr) = acf664940fffc0313c01688209a0d237
ocaml(Constrexpr) = 001812fbe88649fb85bc1e1063d17af5
ocaml(Constrintern) = a8033a28fe7fca27d16d372e65fed2d6
ocaml(Context) = 3fe7fbe659a4f13008383d4561c31eb0
ocaml(Conv_oracle) = 710e6424928355e4e79f94fc54e3996f
ocaml(Cooking) = 18a51bbae8bd6cfbdcbbe7f63e3c6353
ocaml(Coqlib) = af23afa2424208686fde11efe7e05e65
ocaml(DAst) = 2f2b7acba36e311950e44668c73498db
ocaml(Declarations) = e11e7b55e2022e146635311703c7f8ca
ocaml(Declare) = d2c0103ef1dc9d638c4f209a7cefc785
ocaml(Declaremods) = 86af76c503a5c17f27d1b57895a1b62b
ocaml(Decls) = ad2128d119f2ee083fd08bc3fcbb1bd8
ocaml(Deprecation) = d7b041802f27786187ee8416dee16311
ocaml(Dumpglob) = 05df61c86fa04d0600215123dc34a560
ocaml(Dyn) = 1b538aaee631897369983bb45811c33a
ocaml(EConstr) = f12616ad158d21a2ed5537e3da0fd5b1
ocaml(Entries) = 511d06092314c189eb1c73b513757058
ocaml(Environ) = 9cb8af3706e624f8843581aa98c3b87a
ocaml(Equality) = b115b42503ec4fb9aa8262153178f5fd
ocaml(Esubst) = 815313524e169289b486f89e5e192bff
ocaml(Evar) = 935cc7677fe970a7206ebfe2e1779a82
ocaml(Evar_kinds) = 4a35778ef84c18690cf246825141e273
ocaml(Evardefine) = 228b2e357edb99df41e0489c0b23d6bf
ocaml(Evarsolve) = a581a8be5cbf80aba6d58be7b0b9c4e1
ocaml(Evarutil) = 47a72ebec653dd2a1a218ef6464ebb6c
ocaml(Evd) = 421312b8e9c7e6fdce6aef8679c651d3
ocaml(Exninfo) = 38ad6517d5220e43e479a1d0d18b8b8c
ocaml(Extend) = 3e9ecbb91300c3df69a2c84e49286afb
ocaml(Float64) = 84d6570848e9511aae54659b18a17c2d
ocaml(Ftactic) = 8401680cca79c824c5b71cc932e9a25e
ocaml(Future) = 056918f0691a7206769938958c112a1c
ocaml(Genarg) = 508690e563971eb655c545a2954a0bba
ocaml(Genintern) = c2b6d5d20ae5122ff92df401a96874f0
ocaml(Geninterp) = 7067c9e7d583f7cf0548275722897c48
ocaml(Genlambda) = 43b0bce21e3927e5e2ad9fe8c9dc1499
ocaml(Genprint) = 5ce4a74c2a2b11fa0102addd6be3e7a6
ocaml(Genredexpr) = 9a8af566f499d25a7d7025c9325b22c7
ocaml(GlobEnv) = c7a9306448899f6209f66dd655affca9
ocaml(Glob_term) = 3642013615c2c0112ce8b70fca2bf9f4
ocaml(Global) = c82a68dcfdf2586e15f7548a15f6691a
ocaml(Globnames) = 24828265b7f1ae3dcf2facaf6787efa2
ocaml(Goal_select) = d1247cc3b0ac79c2f9ffbdcbabebbb2c
ocaml(Goptions) = 937deb56091f7d609729cb85a9c00970
ocaml(Gramlib) = f7a9c352b24c4ddeba559951b0f7dd3e
ocaml(Gramlib__Gramext) = 443690b2317f143c76466a5d3a66eb2f
ocaml(Gramlib__Grammar) = b6f613b5af6e74fccbf4932ead3118a2
ocaml(Gramlib__LStream) = 479adf7cc6f48be49a10d952f395e202
ocaml(Gramlib__Plexing) = d29433cae784e60b04be278488111983
ocaml(Gramlib__Stream) = e34e97e7287f3698c88dac7d11f02272
ocaml(Hashcons) = 16cd719166c8c5010b0670dadb52fe96
ocaml(Hashset) = 054fe5127bf9aac57339f346c0d1a1ef
ocaml(Hints) = b841647482cd3fef24aaec52ad0cc2a7
ocaml(Hook) = 04f6c318e5dc4380e8d89a7074c603b3
ocaml(Impargs) = 6ebc2fdbc25579ff2cc46910f5a9c2f2
ocaml(Ind_tables) = 39b410cf6e73871ee85700ab3cccc044
ocaml(Int) = 9db9b156b240b450eebcce7d49c69088
ocaml(Inv) = 9e795fa84cce70167d1330cc7ff395db
ocaml(Lib) = 47ec689cb28c94f14058358d26142693
ocaml(Libnames) = 17c14327b9e22b508dbf16535b8e9383
ocaml(Libobject) = f566ef24eea0c63237d3c3f167816608
ocaml(Loc) = 66403678cb7815a79c0e1a1c82447bd2
ocaml(Locality) = a4f0d96e768809a92230d1e461bb358b
ocaml(Locus) = 88f0e885b31a8dd39208e2b14fb5adeb
ocaml(Logic) = 2dd074517298492cf3666f61f877c172
ocaml(Logic_monad) = b617dbec58c0edc562650901e5ea7463
ocaml(Ltac_plugin) = df167d955e180cbe1923b3aca1a51797
ocaml(Ltac_plugin__Pptactic) = c6bd202577c8962298f99a38565f9e33
ocaml(Ltac_plugin__Tacentries) = 5a2d1920a346f707cef71ab0d8d2396c
ocaml(Ltac_plugin__Tacexpr) = 7dad1a4e00b4f3c0a8a7b85276991bec
ocaml(Ltac_pretype) = c63e6540f28100332bfc151da2ff363d
ocaml(Metasyntax) = b630613c74b71f1b5f49d5d79ee3ff74
ocaml(Mltop) = 537ad855371b86d53e2f554314bb594b
ocaml(Mod_subst) = 87bf8a9e488a2d66b98b311cd9e9b9f9
ocaml(Monad) = 111c49d5acef9c643936ce9c7f2dfa62
ocaml(Namegen) = d7cfa5e742ed7cd93aa0dbcc494b1071
ocaml(Names) = 012fb1b3a7cfe3314a332d1ca5acf690
ocaml(Nametab) = 1df605c7bad951b8cae34399bc930f27
ocaml(Nativecode) = 10320d3f9e177dc2c8883253f4b1aae4
ocaml(Nativelib) = ca885e8aba83fb0f378e718af379cb04
ocaml(Nativevalues) = 71c6a790ed5749675aad7773ae17fb44
ocaml(NeList) = 970a4fb3b081f410660ba7e487594f83
ocaml(Notation) = 56341c774049f672274e301c53e12656
ocaml(Notation_term) = 23d4f51cd91d7b03965dfa71c2d499ae
ocaml(Notationextern) = 9b4f5d6a8734829b79fa5c35ad263828
ocaml(NumTok) = b0a3b98c1f6a9bd60982ac4e9ef65dd4
ocaml(Opaqueproof) = 38a55fba1df13077948ee92b583d927d
ocaml(Parray) = d7ffd5166e0ad210e99839a7a8859a57
ocaml(Pattern) = f5c4f8fed7d2454c5806df017306bd03
ocaml(Pcoq) = ea2c841c09442e708e0f8a8cc0044923
ocaml(Pp) = a06106912b4260216a95b51835f39c2e
ocaml(Predicate) = 1b54ffe866048b283dcf39c247b9f856
ocaml(Pretype_errors) = 1d0a44b2a2d6f9e290fe733e60bff375
ocaml(Pretyping) = 8c7597fa2cac52e76bd458219483c86d
ocaml(Primred) = a2a70f50cb0abf7070f6d70f32e1af58
ocaml(Printer) = 7a19633a5ac20808f8a4b826012915ac
ocaml(Proof) = 33a8a89b8674f99fcff5ad7076a118e8
ocaml(Proof_bullet) = 8866137c53fe7e92b68bcefc4b78c9d9
ocaml(Proof_using) = 791e55bc95f9956363dda1074e7c939a
ocaml(Proofview) = 539ebd2b6bc29156327ec1b098209181
ocaml(Proofview_monad) = 9cf42adffde2d967be09cedb88fe9c17
ocaml(Pvernac) = a0e7a205ef7ee4bd4d4ff5846012bb37
ocaml(Range) = 63247554a25737029029a5ce190b7152
ocaml(Redexpr) = 7f4803a94320953997ff3430a70c62a9
ocaml(Reduction) = 0bb6d8efa644c9bbf5faebe969e316a8
ocaml(Reductionops) = 214e513363c495db0adb82ed78d9a803
ocaml(RetrieveObl) = 7f21b7a5114e080ee84528e731ba6f65
ocaml(Retroknowledge) = 2acb5320cf7ecf9e2f3efdc0bdc1d99d
ocaml(Rtree) = 3070acfe312150638de5f65e9e319e64
ocaml(SList) = 3db7c318198c7d1af831076050e784a4
ocaml(Safe_typing) = f0c7eeeaf667d13dbc8a0f3cd6047d0b
ocaml(Section) = 4d882372f334b74c5b84c177f7747048
ocaml(Sorts) = cc9f372946ba5f59c2897e02518b0d22
ocaml(Stateid) = 54380a42612c023be92895eb75e54315
ocaml(Stdlib) = 85f85ddb47edc0c7579657eee740302d
ocaml(Stdlib__Array) = 9bcf1a06bdcfbb976f898e818e15611a
ocaml(Stdlib__Bigarray) = 55a812d9a3c89e7a8ebb917e63e4beea
ocaml(Stdlib__Buffer) = 12b944b4b2913751cd65bdc638975d4d
ocaml(Stdlib__Bytes) = b0d2a0027e7278e26a1fe4bc0e79a690
ocaml(Stdlib__Complex) = d5f041ccbe9783af90ca38337002fb4e
ocaml(Stdlib__Digest) = ff876226ab2584c79cfe1afd26ca2f58
ocaml(Stdlib__Domain) = 0d152be3cd9163970a657d842fca8ecf
ocaml(Stdlib__Either) = b3ad0f8c65f28252059edebc03f68808
ocaml(Stdlib__Filename) = 218e1f57bdea9d296a9f66e323e71029
ocaml(Stdlib__Format) = e7385010d0d6a0bbd4191bc7546d458a
ocaml(Stdlib__Hashtbl) = bafdecabd3fce4f5ccc09a1a5587dab4
ocaml(Stdlib__Int32) = 1db604c2106f996ea47a572773a5ff7f
ocaml(Stdlib__Int64) = 7ab3f2ace09cfcc67be8a7133d18f0e2
ocaml(Stdlib__Lazy) = ca3d5c326131437daef18ae34e7f4aa9
ocaml(Stdlib__List) = feb7c568830f9f239501efb83f4725e4
ocaml(Stdlib__Map) = 71415964978d1cf0c1701af1137aa1ea
ocaml(Stdlib__Nativeint) = 627e6e1768175d0dea895dfbcbc11457
ocaml(Stdlib__Obj) = 85655eceec5bcd6c7c4ef5dd6758b19d
ocaml(Stdlib__Random) = 3f2ddc04bb28ff1050c0c8d7cf5a8d57
ocaml(Stdlib__Seq) = cc3f899885b746f777815dc93be7ede2
ocaml(Stdlib__Set) = f849884bcf48f894e90800c7ccd98f21
ocaml(Stdlib__String) = facad7e0dada5941148738b8188d844f
ocaml(Stdlib__Sys) = a0375c47cee9c7e20ff8f61d4f04e748
ocaml(Stdlib__Uchar) = 9ea864085095970c73b7b17c26c37317
ocaml(Store) = 63270e261706eb1cea0ca37b342126b2
ocaml(Summary) = dc1c2505d9b1f77b75c6aca426effa7d
ocaml(Tacmach) = deb977ab888afefade68e53a1030f984
ocaml(Tacred) = 251ae9ed0fd6696c3aebd5d914cc64ec
ocaml(Tacticals) = d9c3c068a9ec0363e46738dc9b8e23cf
ocaml(Tactics) = bc99036b575021c9469a54f7cdffa366
ocaml(Tactypes) = 46cd140832db0a4b9b5c3813f1f2b415
ocaml(Term) = d1d85dd60ebc47c2ab7926343361de62
ocaml(Tok) = c7e17493652fa46ec713b60e9fc08fef
ocaml(TransparentState) = 7823591e24f8fe112e1e16e79655d585
ocaml(Type_errors) = ccc6b095df0172e70996c28a46a055ef
ocaml(Typeclasses) = b2e4186412dac99a2430de9d4fb3337f
ocaml(UGraph) = 27ea9b0119ade4eab3827ab655b4694d
ocaml(UState) = d548a2a4bdaad5a30afd65583788dd7f
ocaml(Uint63) = 69f038589ad8461f82667721d319bc09
ocaml(Unification) = ce2d4155b080b7ce63bc49841bfd3efc
ocaml(Univ) = c7f67b2c06faaeeac37d4134d85684a7
ocaml(UnivGen) = c66e7e99afb88a1b75ebcaa1a84a5eb0
ocaml(UnivNames) = acfb4f75dcc88c28bf984b666dfb2c68
ocaml(UnivProblem) = bf1fcc3d4d632b787dd90eba436e288b
ocaml(UnivSubst) = 36b66b56cf5c40a7e66f709a7e16793e
ocaml(Unix) = 8da0575524ccb15782c0ca7ebc83ccb8
ocaml(Util) = 4e2d66cd8854d72d19ca403ade93245b
ocaml(Values) = dd4b54c7a63002dbbaf42b63ae2c0422
ocaml(Vars) = 83a744e387e1a9296ab828829f307cd7
ocaml(Vernacexpr) = 4819a3602643a6a28fcd1293bc081b14
ocaml(Vernacextend) = 85b8597350f5136edd4d4f835e8ca307
ocaml(Vmbytecodes) = 901eac76543c714b27471d77c4300db9
ocaml(Vmemitcodes) = 914f5a6360e08c57a373d1aea72b8c44
ocaml(Vmvalues) = d45c240d6b251288e3668fb3c0027bd7
ocaml(Z) = 0009d1c1f4074c1e5cac1497b3dc94fa
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)


Content of RPM :
/usr/lib/.build-id
/usr/lib/.build-id/2d
/usr/lib/.build-id/2d/bf4042497823eb078e8ed6b3f5584ca3b70b39
/usr/lib64/ocaml/coq-gappa
/usr/lib64/ocaml/coq-gappa/META
/usr/lib64/ocaml/coq-gappa/gappatac.cmo
/usr/lib64/ocaml/coq-gappa/gappatac.cmxs
/usr/lib64/ocaml/coq/user-contrib/Gappa
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_common.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_decimal.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_definitions.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_dyadic.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_fixed.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_float.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_library.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_obfuscate.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_pred_abs.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_pred_bnd.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_pred_fixflt.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_pred_nzr.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_pred_rel.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_real.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_rewriting.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_round.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_round_aux.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_round_def.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_tactic.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_tactic_loader.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_tree.vo
/usr/lib64/ocaml/coq/user-contrib/Gappa/Gappa_user.vo
There is 6 files more in these RPM.

 
ICM