SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

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

Name : gappalib-coq
Version : 1.5.4 Vendor : Fedora Project
Release : 3.fc40 Date : 2024-01-24 13:38:56
Group : Unspecified Source RPM : gappalib-coq-1.5.4-3.fc40.src.rpm
Size : 2.14 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/40/Everything/x86_64/os/Packages/g

Content of RPM  Changelog  Provides Requires

Download
ftp.icm.edu.pl  gappalib-coq-1.5.4-3.fc40.x86_64.rpm
     

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

Requires :
coq(x86-64) = 8.18.0
flocq
gappa
ocaml(AcyclicGraph) = cdfee4e5829f040abf5ec1cb4d0fec46
ocaml(Attributes) = d6359250e0a3423187e8cc5344815e8d
ocaml(Big_int_Z) = 664aafcb7c2f819c294cc854657087d3
ocaml(CArray) = d0b8e142800441f2986abc6a10b17d96
ocaml(CAst) = 71b4519533385925ca69635a553e0698
ocaml(CClosure) = a70816f1562d0dfd0802006a5ddf258e
ocaml(CDebug) = 5e34d27037ef21338a8ad53fef60fa9d
ocaml(CEphemeron) = cc49b32dce287834ade5fa01506b4897
ocaml(CErrors) = bf0d4fa7b58ca1ee217d37e29d8b97e0
ocaml(CLexer) = 9e9bf29f256743ed0bc49effa3d9ef47
ocaml(CList) = 410a49e74c519628da742b743c5d1505
ocaml(CMap) = fb01a8a4b3e562cc65968b1a64e3a886
ocaml(CPrimitives) = 0781761bf480e3b408e0819e32edafb6
ocaml(CSet) = 93611ef3700d6a8f15a80498b188afc1
ocaml(CSig) = a79321778c76160b752610c73719a509
ocaml(CString) = f37e3443177ea99478cea5cfc3b151b8
ocaml(CUnix) = 8c5a6c99a70b4a0f057c7468f74f5475
ocaml(CWarnings) = 84dc96e3d7ef74d984dc274a58bcf663
ocaml(CamlinternalFormatBasics) = 2125f26b831153c92a44f06bfde570ae
ocaml(CamlinternalLazy) = 24528204a58c2912a77812f0a2439856
ocaml(Coercionops) = eef0dcbfc9084d617a769fe3ec3f933e
ocaml(Constr) = 71385776dccfc85584fc72bfd346d3d6
ocaml(Constrexpr) = 702772f5b863684cb7f922d55dae31ed
ocaml(Constrintern) = dd1f69f8dad4a12f555141938638474d
ocaml(Context) = f520fe433a2e42ab83cf427af998339a
ocaml(Conv_oracle) = 95d6fce63a260f91954d793cb98df0ba
ocaml(Conversion) = 9e9626c34d09767f7c1d9e52524bd341
ocaml(Cooking) = 13dab310193784c2e27c500f952c2eb5
ocaml(Coqlib) = 27e2a48f81dd9ee0f7f7a0be7eabbfc6
ocaml(DAst) = e02fc82907b86e6986088bccf10577d4
ocaml(Declarations) = ef896e131e7724b6a67a5e7b08cea3af
ocaml(Declare) = 0a64688bb4b9f5be85f07f41be62c517
ocaml(Declaremods) = 13647ca83c90ef6f11def84b5e9dc6b3
ocaml(Decls) = 8c437b248e3fd799b4ba683b998bbb81
ocaml(Deprecation) = e23a92f5be3bc039fe40f761daf486bd
ocaml(Dumpglob) = cd2c601512b598965e058ef3d417fd3b
ocaml(Dyn) = 837a60cd76e63607781b264b2e3f3ba9
ocaml(EConstr) = c961579c9d3b4e04c956d0064ca6d329
ocaml(Entries) = acc9c6dd41701b5f7bae8d4315223b70
ocaml(Environ) = ab629d39e53c035a93494ce158feb6cc
ocaml(Equality) = 4d9dc7525d3d143b1d7340d2b23979a3
ocaml(Esubst) = e4717fd1e0707d98d442c61e0a5b8297
ocaml(Evar) = d3dc6bccd89a24c2ac00f677d10960df
ocaml(Evar_kinds) = 174cba84da7dfeddb9c6dcc868037b15
ocaml(Evardefine) = b2a752c79ef20159d73c9714ce99e313
ocaml(Evarsolve) = 0026e4107d6ac709e5ad7f18dbc7b8b2
ocaml(Evarutil) = 05af8465a44fdf73766920fce88a1689
ocaml(Evd) = d3cd70c1d8817206ef6f4e8e6172c4af
ocaml(Exninfo) = ea79c74e37f7cacfcd3199d63fc1b297
ocaml(Extend) = b3262157a35606f512a81501e073a8ea
ocaml(Float64) = db0513c3d78747b402371a1a1ec6a5c1
ocaml(Ftactic) = 4baccd80f1a2a0c9ca9c316fb44cce3a
ocaml(Future) = 9e621cbecb105580c34f8cf9f081fc73
ocaml(Genarg) = 8f340f0198c405739c88c3b9f7083309
ocaml(Genintern) = 984163133d6eebc58de054a2c0946567
ocaml(Geninterp) = 325397bfbd9f04bc3be064c77c55041c
ocaml(Genlambda) = aa7d18f18dde8853a9dbdd3269864b49
ocaml(Genprint) = 8f70360eff9f2bd3bbecdc48ed83abdc
ocaml(Genredexpr) = 727acc8f0760566749c350a8734fc60c
ocaml(GlobEnv) = 2898136f6b0652b7c19189853cab05e7
ocaml(Glob_term) = a53d61e3a0992e155f24e8d154ec994f
ocaml(Global) = 3f239c3db046a571bdd1a0649b80a266
ocaml(Globnames) = 5704ac54d6b548dce8a04c53570682e2
ocaml(Goal_select) = eb24af1774b2c22e49766c7a05d3ad0a
ocaml(Goptions) = 693e52743db76799be90eb75f8f72a65
ocaml(Gramlib) = 9a8fd2651569f6b0e0c2dcd907918b41
ocaml(Gramlib__Gramext) = 42ab6f41acd4bb3eafe9519122b0544d
ocaml(Gramlib__Grammar) = 7a7555b2729fea4e430f5f684b54f097
ocaml(Gramlib__LStream) = 428f949440104dc0779bdfbddae00204
ocaml(Gramlib__Plexing) = 1cc86a0347c6b7b866f39461140ba0ab
ocaml(Gramlib__Stream) = f85c48cd5f3736fd8892c81fa5153d74
ocaml(Hashcons) = 22f4795de199b84d2df6ec0af1bbef10
ocaml(Hashset) = 6b079efe00409f0ddfefcacb46fb2dcc
ocaml(Hints) = 07825d485c742883007dcd894894faa6
ocaml(Hook) = b7c2df039ba9272cbbf0613b45088b36
ocaml(Impargs) = 15c5c7323e0d6db98d22694859858a2f
ocaml(Ind_tables) = 9e367875834387b0def2b2721f442cc4
ocaml(Int) = 0f78938e5328ce3abc227dd05cce0e0a
ocaml(Inv) = f9a05f0c0a31ca43ccab18112419e28a
ocaml(Lib) = 381215d214882495a43d0702da1a5258
ocaml(Libnames) = 66701935a7a2d19989a1a923f6c103c6
ocaml(Libobject) = 847d74e2686cd54cd2aca770630c7e81
ocaml(Loc) = 1aa3693c0002eb1a9e83bbb3131e3061
ocaml(Locality) = cc8672e3eb2710c5d772d285f2e25525
ocaml(Locus) = 5f020357f6b5e1f255668be2b0aec049
ocaml(Logic) = d6eaeadf0ec593a59e662e24a3a4f55a
ocaml(Logic_monad) = 829da051a3765189b8e032d18018dc69
ocaml(Ltac_plugin) = 9535c9941946ac241050beb63162342d
ocaml(Ltac_plugin__Pptactic) = 1dcdcaaa8c336599c5f72de39afd315b
ocaml(Ltac_plugin__Tacentries) = 6f14d98c08d086c480967aec57599320
ocaml(Ltac_plugin__Tacexpr) = 6c4dbcf45353423c8ba0465ff07c805b
ocaml(Ltac_pretype) = e022a712693a55ac3ebc80240dfc1454
ocaml(Metasyntax) = b144930a3f698bc1ee20121e295cf45c
ocaml(Mltop) = 3e22ef583bcd1d3024cf3257848d8d9d
ocaml(Mod_subst) = 4fafe132554487dd9a55a12fe796ec0a
ocaml(Modintern) = 46de56f6528f7b0af0043b3b3b0b1adf
ocaml(Monad) = f4ab549dc270bba095c37b84de14fd94
ocaml(Namegen) = bbdee054ff14b4382dd42aa483b19d78
ocaml(Names) = 50f6f1b8efe16612d33d2cb49ced8446
ocaml(Nametab) = 3112a3fee1d9381944491b3151c6868c
ocaml(Nativecode) = beb9ff066d0cd2a38a527af7983833b7
ocaml(Nativelib) = 56efcd593193453a2cb0c4487994337c
ocaml(Nativevalues) = 383a071965e2632c01ab92236cd2ab98
ocaml(NeList) = 24834dafc4f5a1cf810c3f9eaf8aa0f7
ocaml(Notation) = f3db292cdca076e60924f6bcfcac9893
ocaml(Notation_term) = 350211d962c16e633eefefedf41fad3f
ocaml(Notationextern) = 001662356074865dc0663483bbc098a0
ocaml(NumTok) = 7664175efbf442a691279cc42d301ba9
ocaml(Opaqueproof) = 5201a243c8b273864fcc3e51de258251
ocaml(Parray) = 27786cb5f50c7da3da038db7f56fec6e
ocaml(Pattern) = c3438c57623d16ded0e35e4b0314d758
ocaml(Pcoq) = e79edf4dbc025f4a9af0b0021670f39a
ocaml(Pp) = c495dd6f22a2ed429fa0d09a47c82de4
ocaml(Predicate) = 61a5246feac0f5e76d6437e94009b3cb
ocaml(Pretype_errors) = 9be5c9b0a3eacb437fe38dae6ac7c848
ocaml(Pretyping) = 97a0bf95954666c3ab67bd9c0da66ebd
ocaml(Primred) = 9e47c0b6e0c4902aae795f45a50c8943
ocaml(Printer) = b5b9924caa7ee12c6f9a5897115ade05
ocaml(Proof) = f91ec867f8a46f260953840d546cad36
ocaml(Proof_bullet) = f9b33dfd67d395d409d95f30b3c56bb3
ocaml(Proof_using) = 0fa2161f5998d0e73b0f8c3ba3b1fbc4
ocaml(Proofview) = f58c551becc7c726f29cc75947fa7441
ocaml(Proofview_monad) = dac4bd5393d881dde7e076e44f182aef
ocaml(Pvernac) = 1e7a100249e9c3d91a5043359328bafc
ocaml(Range) = da820172ed0d90aba4156c9bc48f7367
ocaml(Redexpr) = b5fa6f860701f22b249529cce2221830
ocaml(Reductionops) = b31750da9255680e4953c4431f717e23
ocaml(RetrieveObl) = b5281635d67a182364f62e4d0f2e69d2
ocaml(Retroknowledge) = af103488193ab7d811d1b0dabc521717
ocaml(Rtree) = edbcc00d1123e2a43e2b54c8f7f1a916
ocaml(SList) = 9ddb9252f133868c2025b4ea84ee6ad4
ocaml(Safe_typing) = 29fa3fa49184f17fba98682b9122ed6c
ocaml(Section) = f5cf08158e763d9b2377f67d22346206
ocaml(Sorts) = c8c151ca2e00be7dae00401ea367cae6
ocaml(Stateid) = b7a5f7a67e05112eb3662eb26eff2889
ocaml(Stdlib) = 0b4549228bc9b8c1cfa1e888d7432bdf
ocaml(Stdlib__Array) = 52e44fdea03eac380addda1bf0f21120
ocaml(Stdlib__Bigarray) = 7c919af812ad8dfb0033b8dde0d08c07
ocaml(Stdlib__Buffer) = 11209f45e0193c65ddf3fa42e62ca351
ocaml(Stdlib__Bytes) = 4386c229afde8970cdf6f40df1a450d1
ocaml(Stdlib__Complex) = e64ee90eddc7b10ec8fbe26c11240f8e
ocaml(Stdlib__Digest) = 17051ff52cc6746e479ab37505a0e4bc
ocaml(Stdlib__Domain) = 15eb47920ac7664c134360a87b41ef28
ocaml(Stdlib__Either) = 4c7aace90230bd854d0973c7e456ef08
ocaml(Stdlib__Filename) = 7aa3d26ec3f7ff811d5349b4988d6820
ocaml(Stdlib__Format) = 94d7f939ea070018aea40586f319a4ee
ocaml(Stdlib__Hashtbl) = c04858fec86768f735bb82b2552d3868
ocaml(Stdlib__Int32) = f83b5c153cc85f2fcd7b605b4364096f
ocaml(Stdlib__Int64) = 4083d22bff8ac50e44fcd319f4c95a1f
ocaml(Stdlib__Lazy) = 9339b146fb57b73e973430d5ffd6c52e
ocaml(Stdlib__List) = 8992587f26a4ebfea5772490b254b328
ocaml(Stdlib__Map) = c10b896173aa2c544de555b28ee90050
ocaml(Stdlib__Nativeint) = a7cfe093e92b186c7805358e8d76fc8a
ocaml(Stdlib__Obj) = 111b50f0cfcc8a94d252818567fe891b
ocaml(Stdlib__Random) = 14055871ab1ada985887fe17857a4bc8
ocaml(Stdlib__Seq) = e469865a3128bb838ded5895e9e9e56c
ocaml(Stdlib__Set) = 377c5c852dd2b05c647cdf11b66f92ab
ocaml(Stdlib__String) = 8d7e7cd15035dc5d921d9985a1f7d0a3
ocaml(Stdlib__Sys) = 35430876c7d8c929086fdca8efc73e48
ocaml(Stdlib__Uchar) = bd0ab58d166b896b51c953631e3a39c5
ocaml(Store) = 2f6454fc91b37071d87bb5cebe4b2b55
ocaml(Summary) = 944787e2184c33f6151c5592a460fdfa
ocaml(Tacmach) = 9ad0d947d33202ad6213639e9c06bffe
ocaml(Tacred) = 85648f83307a1eede8020119938cd73a
ocaml(Tacticals) = 21a7aea970e9ad0daf283e1ac263402f
ocaml(Tactics) = 379a3f75a9f1be52f5bb991447451dd7
ocaml(Tactypes) = 8f45872ac3979048974d0b2824119fcb
ocaml(Term) = 2fbd6c63bfcbbd4e5ded45d2cad45f4a
ocaml(Tok) = a2c4b487db0eb8a53bcf19d7b067bce1
ocaml(TransparentState) = 831b7b89c303278f6f19f6b48b5f3b91
ocaml(Type_errors) = 379da22dd64dcec4e4bf057686b19086
ocaml(Typeclasses) = 4b4f813778c0d2e701b6346c87c0a07c
ocaml(UGraph) = 9c4aea680459b33e4d89c02081bf4a2c
ocaml(UState) = 5344cbd77c880afbefd094d7430aa705
ocaml(Uint63) = ccf4e2651d53bc5f2ea1ee89888aecc0
ocaml(Unification) = 111b9d3dffbf344c14d5689a2edb05aa
ocaml(Univ) = 631d6eb7573e8a3ee3a594284a544ae3
ocaml(UnivGen) = eda2aebf2aa2f3121853f11ba01b0043
ocaml(UnivNames) = 25975fd1252b4a4d246e01e8c26eb24e
ocaml(UnivProblem) = 3627a112b5012efd008d6136abac379b
ocaml(UnivSubst) = be71751f6d6382b503475d8422db6d29
ocaml(Unix) = 3a423732520b05536abd290bef5048fe
ocaml(Util) = 74bcae9f40763d8877bc3099e822ff48
ocaml(Values) = d7ad0b27a83baaf5bb6b915f0623f0b6
ocaml(Vars) = 4c5da64b5ab4e204f1baa3a65d97fafe
ocaml(Vernacexpr) = 4c757c671c186ac100eaafd126d35d89
ocaml(Vernacextend) = 490815a74fd2a6befd19122f9919d904
ocaml(Vmbytecodes) = 1915978944789557ec2b5b8f66d0a010
ocaml(Vmemitcodes) = 7743648aa59e4444f16748ec2ed2c5f7
ocaml(Vmvalues) = 2c38ece8d1f5259988edd040477dc511
ocaml(Z) = fdc4d8381bc74f86dcda1f279434e96f
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/b3
/usr/lib/.build-id/b3/2962149a48175652e50fdfd3d939838c32fdac
/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