SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

gappalib-coq rpm build for : openSUSE Leap 42. For other distributions click gappalib-coq.

Name : gappalib-coq
Version : 1.4.0 Vendor : obs://build_opensuse_org/home:ptrommler
Release : 1.1 Date : 2018-10-11 13:46:14
Group : Productivity/Scientific/Math Source RPM : gappalib-coq-1.4.0-1.1.src.rpm
Size : 2.37 MB
Packager : (none)
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: /packages/linux-pbone/ftp5.gwdg.de/pub/opensuse/repositories/home:/ptrommler:/formal/openSUSE_Leap_42.3/x86_64

Content of RPM  Changelog  Provides Requires

Hmm ... It's impossible ;-) This RPM doesn't exist on any FTP server

Provides :
gappalib-coq
gappalib-coq(x86-64)
gappatac.cmxs()(64bit)
ocaml(Gappatac)

Requires :
ocaml(Ppconstr) = 9840b67d819fb2657e3a5db2b1022834
ocaml(CAst) = 7f78dfc5490aaacbdce6f32feb1b5fe8
ocaml(Store) = d332b664fa56640cdcdd288f196d83ab
ocaml(Array) = 3e56b0036c5d9e653763f3450236560d
ocaml(Nametab) = fa040126bd300a5e2e3a502e0c7827a8
ocaml(Elim) = bdb3114b6160a832c3600dcab2d92ba4
ocaml(CPrimitives) = 474807c51594d0a378ca379df27c030e
ocaml(Retroknowledge) = 799dd8bd180ac440c735acd801419ed4
ocaml(Stream) = d0b21ad0c1f4e93fa8c05b9ded519b52
ocaml(Smartlocate) = cfea9d5aea18c6c2b2aa176dd841e70b
ocaml(Reductionops) = 3eab68fa8e130bbecab45068b78881d6
ocaml(Loc) = 1453106bd442b16164ca8a046d1f7e57
ocaml(Grammar) = 65ca355f8029e4a5c3e317e5a96d964c
ocaml(CString) = 4322fd69ea289230213f0f13b4a4a850
ocaml(Pattern) = 2d0a84c4766343bce900405bc4387e10
ocaml(Type_errors) = af76439d504284cfe433af57532340ad
ocaml(Entries) = c128a648a60b642604f617cdca8aa314
ocaml(Impargs) = b7950cb664246c09ae2175f267375432
ocaml(Declarations) = da1af352e3655022cc7e58ef6efe2fa0
ocaml(Class_tactics) = caa22861127ab22742dfa6b0e39e18f5
ocaml(States) = ed162cfdd7e1e6889f115c3d61cabb4b
ocaml(Int32) = d0de3bfd44513ff6fd70cbf476e9fa55
ocaml(Pfedit) = 0c3f38b1a7cae2e759f1dfff78abf14d
ocaml(CSig) = ab054e4f2ccd0817db07d5100a69e280
ocaml(Hashtbl) = 049026f8240c3b61bd91f719b0f55877
ocaml(Declare) = bc10568d9141263eea3a726ea8850c4b
ocaml(List) = ac5f6095cc0a546330ada0df0986a497
ocaml(Uint31) = 0b632be11d005ec9d1a73ce314c7da13
ocaml(Constrexpr_ops) = 1febb597a64ae2a0899d8469edb9c488
ocaml(Evardefine) = 4b4fd5049f4efa4f1f7804025eda9e4e
ocaml(Conv_oracle) = 689ea1b1b729116d0846ec874eb877d7
coq
ocaml(CErrors) = a3a83b8bc3edb46fc137c35d1b2efab1
ocaml(Lexing) = 330cec55af19abb867bbde7885b2588f
ocaml(Goptions) = 55341663b9f485f079cf5d9e2dcc6d9c
ocaml(Auto) = 51e1bfba2a67ed0e5a0cfee870171290
ocaml(Redops) = 6d89444d4a76602ef538f773cd43be47
ocaml(Nativelambda) = 4c8753afd129dde896d3d9259d1b84cb
ocaml(Hashset) = 64604190db42f607509eebda4939f786
ocaml(Pretyping) = ea4f9049f0b26738f8f6e262dcfa7df8
ocaml(Tacmach) = 4725fffcb6bb0dbc77384b1c8a1510d8
rpmlib(PayloadIsLzma) <= 4.4.6-1
ocaml(Proof_type) = 9a24ee8dc366c2df2a3e6237ddd1ae27
ocaml(Genintern) = 21d00dd6ef65798f6632639fa3a9730c
ocaml(Extend) = 181a430c6eff092ab2621412e85ac951
ocaml(Ind_tables) = 80b4d305683e8f40434fcb86acf8b9f0
ocaml(Constr_matching) = 1200c1a1b9f0830f1d0dfcf8ee7dbcff
ocaml(Tacticals) = cb14302b0a61be618c681af1d8ab4efd
libc.so.6()(64bit)
ocaml(Digest) = 23fdbfc720a71002434f407c37d040a3
ocaml(CClosure) = c9d777974150b1c3bf2d9ea56d38395b
ocaml(Evar_kinds) = 8d6932be64384533ad99eda67b7da9f9
ocaml(Mod_subst) = 669facd81aab62eedf859e81fd410777
ocaml(CSet) = af2e6839ac7fe23b578b83712c2cee4c
ocaml(Unification) = 891bcd9d0841e1edb517405fbc1d0c13
ocaml(Constr) = f72db12ce859bb08e5b163508b6f061b
ocaml(Stdarg) = db1eb7168c0f022740a9f1fc4349cfa5
ocaml(CLexer) = 70e86136ef6ec9f0d5949e7a5f115937
ocaml(EConstr) = c5382fa85928945047426c028554cf19
ocaml(Map) = f23f0e2510f18d4b11ad6f7771618294
ocaml(Glob_term) = 7b0e436bf9709a12c2d2879ffcd278b7
ocaml(Tok) = 044de3acea4b7cc188202d4c0c51ddd8
ocaml(Globnames) = 73947e04fb0780636bc0a7895366a63b
ocaml(Context) = 5905a35a1c0e3b84675665b3bf0accac
ocaml(Egramml) = 43d82d250f9c29b66e566bb7f480e206
ocaml(Hints) = fe6c4ccdcfc5bc23327ae1ee5c81bdab
ocaml(Locusops) = e37c531a15891a9415b747b3471096df
ocaml(Range) = 6ef72f2fb5b8169a3775dd3bca35b541
ocaml(Sorts) = 36042c6a428c05056af16f41568b10f5
ocaml(Proof_bullet) = 1d79bee7f8af75e28890188d87c01da9
ocaml(Pcoq) = e07e7c2a7b4a33e5ee470a1231985891
ocaml(Geninterp) = c47d9e608a5c2f75f8340a50810c83ed
ocaml(Autorewrite) = a5b2366b604623d7164e1305b2d39d99
ocaml(Equality) = 823c7010a6d55a43fe11795f0cb8bac1
ocaml(Evar) = 6b454349ab0070d29a242b5b05053262
ocaml(DAst) = d6120e0b19478693e9bed652d91bc3fc
ocaml(Constrexpr) = 3f753370ecd9cd027b0b206e7223c129
ocaml(Environ) = 0e3cd849bda0e347bbdb4666522a16ce
ocaml(Format) = 60c2e7663dd57d13b5920931742e1c10
ocaml(Classes) = a0fad0354b56d328d427b0a089f2fca8
ocaml(CEphemeron) = 25d098cc0ae7c4e17af66208c398b52d
ocaml(Ploc) = 0b4c310139b980f638b42d05a559f67e
ocaml(CArray) = 78898aae3238909361b61a9405e1f9af
ocaml(UState) = 259d57b8a05d1d38f48c481a72cee7cc
ocaml(Vernacinterp) = 222d7b266e80e4b4e0b79761e9fe47ec
ocaml(Cbytecodes) = 3aa45bb5fc324b93c02c1a1056947613
ocaml(Fstream) = 588bf4e748839ce9b453cc1a628d6fc3
ocaml(Vernacentries) = edde12a22c4df8f84663be70d54ab2d3
ocaml(String) = c28a3ca42a30c6ffa0bbab4a05329226
ocaml(Genredexpr) = 6c1a7295bde6b1fb5dad6166052cca04
ocaml(CStack) = d3d700953d3b9e26009fba7ba909dc08
ocaml(Exninfo) = 96ad975287f7d96f503d60217d0c31e9
ocaml(Rtree) = d4cb3491cfee59a55073b2329dfe6f53
ocaml(Proof) = 6be358a75495abd0636c4c25a4b74bbf
ocaml(Cooking) = 800021f114b889dca1c1d38cdf9e379f
ocaml(Flags) = a97158a984da0e260b053f5f67a1d50b
ocaml(Obligations) = 2b60af2b2261f79f53bf8a07bf008d5a
ocaml(Locus) = 862c8764b4a079aef8dc6033a6f17d4e
ocaml(Tacred) = ce16f470c08e09b4df8510ffb4bdb48b
ocaml(Printer) = 0836f8cbbbe0f8256044fdaf97de3f1a
ocaml(Reduction) = 58b5377d9786000d75a4631d4b6b85cc
ocaml(Esubst) = f43f9ff027da0d5a561f911786b6a975
ocaml(Redexpr) = 6fe5159c8ba03241dc655fcfee0844cb
ocaml(Dumpglob) = 6d4fd3f3eeee28afcc449c4770325ea3
ocaml(runtime) = 4.03.0
ocaml(Vars) = 40eafbadbba646feccd391cf778aa207
ocaml(Ppextend) = afc96e4f7265d1ad08cdd928ee10b063
ocaml(Int) = 84fdb15cfc422dd48e33262cc3863a8d
ocaml(Feedback) = 4ba8e03d10bc82f876adc81941f5bf6e
ocaml(Stateid) = 03b10914a13523f8755bfb7a3e573fc8
ocaml(Constrintern) = e21667bd306ca617be55028857732bf7
ocaml(Buffer) = 3bd1af04573ce2da7fc3dc04403e852e
ocaml(RemoteCounter) = 6d0d3cfadd4e80cfc6e2aae1692a8266
ocaml(UGraph) = 0430456327f8ce919ffa67f6ffce919d
ocaml(Evd) = a7127e4f1cc9ce51c7e2ac9d950d8615
ocaml(Hashcons) = ad9b73f2e6afc3140ae037133e38a7cb
ocaml(Nativecode) = b636bea2e5eaea00a4bbf1994955316e
ocaml(Tactics) = 4e3d265b75e122cc32da328a6b1ce272
ocaml(Opaqueproof) = f8a4e70b581f53ce2ae1b827bfb495ca
libc.so.6(GLIBC_2.2.5)(64bit)
ocaml(Nativevalues) = 5d19f9781d0dd3e2ba88c7de70b7fd4a
ocaml(Notation_term) = 3f25ae28c917f8e4e1759cb34a666b0f
ocaml(CList) = 92d6eefb0eed6d13bde099b43e8499c4
flocq
ocaml(Evarutil) = 8243a42b610f8faaf213e3f19a6024f4
ocaml(Genprint) = 3fcae3da207e810aa40a6eab4c91a03c
gappa
ocaml(IStream) = b0c941aba53f2662e8e21874c7c472ed
ocaml(Ltac_pretype) = 87596b7ca2389a51bb5e8a6788f0facd
rpmlib(CompressedFileNames) <= 3.0.4-1
ocaml(Gramext) = 7c243720c6c27ac52a3c41ec4af26136
ocaml(Bigint) = 3d35042ef46d760984c828e9000e9290
ocaml(Locality) = 4480d4c429c041d83bf5d3b4de49c8ba
ocaml(Summary) = 948a60a1e0331399262651798b51b36a
ocaml(G_vernac) = d9f8361cfbcd5598b49da31b50077613
ocaml(Eqdecide) = cf68b9fcf8915d8cdec90cc5169a0bc1
ocaml(Unionfind) = 22bf05097fd11e92c9b7504b5965c1f4
ocaml(Libnames) = cb1a77faed19e6d6fd65da89fbcc83bb
ocaml(Term) = 78461de5aa1b07669f063facb0d092d4
ocaml(CamlinternalFormatBasics) = 9642e3ed163e46770985ca668738ed5f
ocaml(Safe_typing) = ed08edf3180dd16e480db55caf6b9222
ocaml(Pervasives) = 999b28e3b7638771c87eebf5a8325e42
ocaml(Universes) = ca8f4a792e6d910d8eb80c34d6d58c7e
ocaml(Univ) = ec20644962f4e8dce143c052762faeb8
ocaml(Typeclasses) = 7e28417ee7876f16ccab4b8249b58feb
ocaml(Str) = fc4cd9c73967ba1a8bc6360b21cf5f3a
ocaml(Pre_env) = b451edc724989f01b6a58af2a36ba80d
ocaml(Logic_monad) = dd5d794b59454907de1de8bd306aba32
ocaml(Xml_datatype) = eff809db921c51e0795a4d3e61062072
ocaml(CamlinternalLazy) = 6f25aad2ca689d32011c428fb8260231
ocaml(Obj) = bff9812925bc903e1896c82e123d0a17
ocaml(Classops) = 1623f6cf7e45d64ca543d9f6fba89d3e
ocaml(Vernac_classifier) = 6a43283815ba19cc785e2bd9c133db70
ocaml(G_proofs) = 532910986350d22d39193fc4a57deb67
ocaml(Pp) = e377764ee97943d1a021b5fc3c0e5aeb
ocaml(Util) = 5689c0e4c92134a5e300a13c64992f13
ocaml(Vernacstate) = 284b483bb8726153f84627985b20fe37
ocaml(Plexing) = 7779eede1b67f76abef54d0650bf1cb6
ocaml(Ftactic) = c59eadb51837269a8bdcf6ba233ca6cb
ocaml(Misctypes) = d1562ad998118eda9280a4a28af48909
ocaml(Coqlib) = b7484023a4665bc70c9607f7679acb8d
ocaml(Option) = 362bc6a4440a44692f36a138078149f8
ocaml(Univdecls) = 0d81e9839ac1f918a9b7f876d340a113
ocaml(Proofview_monad) = 7b2f0d1da78945a695dc4238dfbccb73
ocaml(Bytes) = 6dc691300ced97c0e319cbcc0a715044
ocaml(Hook) = 841244dfcdb29762d9a5f73a89dd409d
ocaml(Ltac_plugin) = 9acfaa78cf0b32c9f631295ae8bc698a
ocaml(Nativeinstr) = 9a05246d55adacf01325deceae1db2ba
ocaml(Cinstr) = 6fde07e99a45bd240cf94e812c11dc43
ocaml(Set) = a16cc25d9afe91eb22559bef41e9ee28
ocaml(CWarnings) = a4701d419d0f814ec968d20ad958f82c
ocaml(Proof_global) = 26a3d4a894a0d8531cfa2ba26c8ec2b6
ocaml(Global) = ebca04302caaaa4059587ac609d00400
ocaml(Monad) = 2013cb45f8a0a21922c4c56d6206b75b
ocaml(Dyn) = 21c42f2d414ea87e9fbc70e38f8e9279
ocaml(Cemitcodes) = 0e962a5e3f134c267dfea3f9305aec28
ocaml(Future) = 80b87b99450e4c43b02a1d08ea3c3238
ocaml(Decl_kinds) = 2da6f7ec624154c4b48ef7005fad559b
ocaml(Clenv) = 36bc928251e25ddea404d44263a46eff
ocaml(Names) = fce3917bff9f98af7d4dec8640d98efa
ocaml(CMap) = 069fa57c2baa24878142f093e2973d6f
ocaml(Lemmas) = e2cc9105c583dc9c5c4d3d4306b068e5
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
ocaml(Predicate) = 044835f939d5eb1963ec7f133d5e1f48
ocaml(Goal) = 0d5de4159735b193d170c53985ccb4f9
ocaml(Notation) = cf4d5df8215351a389b44b0085ca2f59
ocaml(Tactypes) = c6434f7a3b4840ca870ec7f84be2862a
ocaml(Sys) = c9608ce7bf745054a217110dcaac126e
ocaml(Genarg) = 60b72bfc7052d10a9a69b697c6959e53
ocaml(Vernacexpr) = 5260c19c0395ef87f50d01c2efc011f7
ocaml(Mltop) = fded646cce0eceb7647f9185dd3800c7
ocaml(Vmvalues) = c6185dae4378da954b37bc0d5770ab43
ocaml(Eauto) = 087c61045365e538969cf16d4870f8a6
ocaml(Pputils) = a7632814342d6863fabeeec5037b4861
ocaml(Lazy) = b2e565a5cdbd351dc15bc9061d30c458
ocaml(Proofview) = edb228a47227e3f65d68fce841d6a1db
ocaml(Printf) = 0145d8daf24f9afd43ffac3c376fa3c4
ocaml(Filename) = 4d3fda93a4f9d9404ed1832e9422af42


Content of RPM :
/usr/lib64/coq/user-contrib/Gappa
/usr/lib64/coq/user-contrib/Gappa/Gappa_common.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_decimal.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_definitions.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_dyadic.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_fixed.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_float.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_library.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_obfuscate.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_pred_abs.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_pred_bnd.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_pred_fixflt.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_pred_nzr.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_pred_rel.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_real.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_rewriting.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_round.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_round_aux.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_round_def.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_tactic.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_tree.vo
/usr/lib64/coq/user-contrib/Gappa/Gappa_user.vo
/usr/lib64/coq/user-contrib/Gappa/gappatac.cmo
/usr/lib64/coq/user-contrib/Gappa/gappatac.cmxs
/usr/share/doc/packages/gappalib-coq
/usr/share/doc/packages/gappalib-coq/AUTHORS
/usr/share/doc/packages/gappalib-coq/COPYING
/usr/share/doc/packages/gappalib-coq/NEWS
/usr/share/doc/packages/gappalib-coq/README

 
ICM