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.3.3 Vendor : obs://build_opensuse_org/home:ptrommler
Release : 2.1 Date : 2018-02-26 11:43:59
Group : Productivity/Scientific/Math Source RPM : gappalib-coq-1.3.3-2.1.src.rpm
Size : 2.42 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.2/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(Tacexpr) = bfa357cebd0a0499f3ced8c0f49b411d
ocaml(CAst) = 7f78dfc5490aaacbdce6f32feb1b5fe8
ocaml(Pfedit) = 9a50d11330f96a5921acb4ea3455e334
ocaml(Array) = 3e56b0036c5d9e653763f3450236560d
ocaml(Global) = 131cba879726063dc323cec531a278e6
ocaml(Cemitcodes) = 18a3d5f470c7a6ab0c934a8296c4b6bf
ocaml(Eqdecide) = 09745b9abea39f5e2ebd249a97721205
ocaml(Primitives) = 4cedeb4f6c56f2c672e7627031273ae1
ocaml(Equality) = ef9a43447126bd97c7cee8016fb0ba5c
ocaml(Util) = 1772ec80ba57ceff91291a3f0c17a87f
ocaml(Stream) = d0b21ad0c1f4e93fa8c05b9ded519b52
ocaml(Grammar) = 65ca355f8029e4a5c3e317e5a96d964c
ocaml(UState) = fbffacf2965f83437bd69687855897c4
ocaml(Proofview) = 54b011e6382aae6bdfa173afe6ec6646
ocaml(Logic_monad) = 6a9312af72465cf9d24191d417eea281
ocaml(Opaqueproof) = 1bcf1fb434e170e5b0f7e0eefcfbbdae
ocaml(Int32) = d0de3bfd44513ff6fd70cbf476e9fa55
ocaml(Constrexpr) = 42982d5402689a3e182f5a11301f8827
ocaml(Namegen) = 936b4806195dbdc448d1f6ebde80e5da
ocaml(Hashtbl) = 049026f8240c3b61bd91f719b0f55877
ocaml(Constr_matching) = c62565a16f5787d05a8a4ff9547a68e1
ocaml(List) = ac5f6095cc0a546330ada0df0986a497
ocaml(Uint31) = 0b632be11d005ec9d1a73ce314c7da13
ocaml(Unification) = ac9da68875caaec9c062850ea9f28c68
ocaml(Future) = 33076bd9d43185b60a5a1e03e7d0819c
ocaml(Typeclasses) = 011ac92fe1b9ca04a22b0b629ef2a21f
coq
ocaml(Lexing) = 330cec55af19abb867bbde7885b2588f
ocaml(Redops) = 6d89444d4a76602ef538f773cd43be47
ocaml(Locality) = 096a63ca93d434292ab2fd176a4488df
ocaml(Hashset) = 64604190db42f607509eebda4939f786
ocaml(Ltac_plugin) = 39e038b0f2ac57ea2c90231a0668de1c
ocaml(Ppextend) = ffa0d35ee3645dff4ad043486584735c
ocaml(Constrexpr_ops) = 8918a4da4d009f7d381262d9e880d7e8
ocaml(CString) = e81cfd05bec4b309bcdaf894e70b48c4
ocaml(Mod_subst) = efcf1b4445ef6b0fa8c4d713d32b7f5d
ocaml(Entries) = ef3eb6b2214807971eba5237ca50a71d
rpmlib(PayloadIsLzma) <= 4.4.6-1
ocaml(Loc) = a210a0a13619bad90901e55b7a2b5f9b
ocaml(Goptions) = 73b9faf9800edffb43cdc82001b53a6c
ocaml(Ind_tables) = ceac3522a34823b6840485f1e00f0cc4
ocaml(Tacmach) = 6fdc668edb83cf18327dc07fbcdaffd1
ocaml(Pattern) = a13ab3188c897ab5b1d4776c66eeb933
ocaml(Summary) = 7340f87782aa80b8c81c027f03cd4407
ocaml(Vernac_classifier) = fa4d0da57a681afbedf5521b719fde9e
ocaml(Mltop) = 09032deba06d930ba8d14bd3b7773a8a
ocaml(Coqlib) = 9f0d928781e1f216cbd2d32a7405284c
libc.so.6()(64bit)
ocaml(Digest) = 23fdbfc720a71002434f407c37d040a3
ocaml(Class_tactics) = 8a47d66dff70e39408fc093a724a5578
ocaml(Safe_typing) = d696074b995a65e1e1eb5648ab8567f0
ocaml(Reductionops) = 047af2587eec45513e01f9682722e21d
ocaml(Tactypes) = b4807370c686cd306f5d255baec26e9c
ocaml(Nativevalues) = b4710a4bc2d22fd9bd2a86cc89bac840
ocaml(CSet) = af2e6839ac7fe23b578b83712c2cee4c
ocaml(Evar_kinds) = bf30d0c014825f85eb2ef3cec82e5088
ocaml(Sorts) = ace386a33c967680ccb2e0d2bab90430
ocaml(CLexer) = 8642e16bde4f53fce994e6f668fbded6
ocaml(Vernacentries) = b4cf590907a763b2f3a85c50d7b5e949
ocaml(Constrintern) = 17bab70732165a45baa5af1070f8f349
ocaml(Clenv) = 417360297e3426a2c6e93900467b266d
ocaml(Map) = f23f0e2510f18d4b11ad6f7771618294
ocaml(Lemmas) = a5325b6ead0672293623a7398ca90794
ocaml(CArray) = c59e742f060065ad2b5606f04192b002
ocaml(Tok) = 044de3acea4b7cc188202d4c0c51ddd8
ocaml(Evarutil) = cc774c1363b3db8a6f71153c75f00110
ocaml(Stdarg) = 9b8adefbc84a3ed7842ae59212da0701
ocaml(Proof_using) = a157925e8ae582222b09388d45fb2703
ocaml(G_proofs) = cb91de791050ae2385d2784403d44084
ocaml(Esubst) = 4185d2097995d2482d74085f404bd495
ocaml(Tacred) = f7ee9a02c756cd9b82f3b1b6f6b3e207
ocaml(Extend) = fd1bb3c1e7a325088a781bf219648af0
ocaml(Egramml) = fa3dbc22f00e2fd37be729af7d854814
ocaml(Names) = 57c0798bf7b901d99266a79c658e1f1c
ocaml(Ftactic) = 1b7eef0e7f2b7196e2596511f60be813
ocaml(Printer) = ff871c468c8b4f43e4aa5d70adb02538
ocaml(Vars) = b8ac1b00394f6361590e7776f2654fa5
ocaml(Proof_global) = a115f7bda0e119f398b25f5e3bdd7eff
ocaml(Environ) = 71d991e20e149febee85173998777513
ocaml(Notation) = 89a5997e223285e24abcda7b4ae3c9b9
ocaml(Format) = 60c2e7663dd57d13b5920931742e1c10
ocaml(CEphemeron) = 25d098cc0ae7c4e17af66208c398b52d
ocaml(Ploc) = 0b4c310139b980f638b42d05a559f67e
ocaml(Pp) = 9e445778c1ac59cb44c5dad2041e51ef
ocaml(Genarg) = dad80138cb972015e47970baea65e881
ocaml(EConstr) = 9d32afe12ef526f229331a14f0b81186
ocaml(Fstream) = 588bf4e748839ce9b453cc1a628d6fc3
ocaml(Universes) = 9cd081b09ba30529af34ab624597852c
ocaml(String) = c28a3ca42a30c6ffa0bbab4a05329226
ocaml(CStack) = 5e3cbbc1e4a3e50f5280d52efb7f6148
ocaml(Declare) = 62498c76c936f34bcac317cdc362c66c
ocaml(Goal) = f6bc1dc74041903e5db5bc364e740216
ocaml(Exninfo) = 96ad975287f7d96f503d60217d0c31e9
ocaml(Eauto) = 18da209a43bc9d7d62203f47e87a8543
ocaml(Auto) = 363da3dfa0ed3c5d11f2c5feb8fac8eb
ocaml(Libnames) = 5e3127b40131f4060719d60e05bdd8e2
ocaml(CWarnings) = 10a03fb9a761b82fa274962af8defa7f
ocaml(Tactics) = 482d9ccee69a347bbc55e13b6f92ff42
ocaml(Topconstr) = a940fb87bb4e1b64aae3457581de771d
ocaml(Nativecode) = a60671c235666a49646959c99b380151
ocaml(UGraph) = ee042a409ba8a760cee8bfb6fb0027db
ocaml(Context) = a0a5e6c705e0da0414ae46054a7acccb
ocaml(Vernacexpr) = fb433baa31eece79ef3205bd10585e5f
ocaml(runtime) = 4.03.0
ocaml(Proof_type) = 3ebd6edbe13b5bdb42d3ede4f92936aa
ocaml(Notation_term) = 6619f355aa38dcd02a928cd37d94410a
ocaml(Vernacinterp) = 876be2409a35f12c03fc688ffd8e73e7
ocaml(Stateid) = 03b10914a13523f8755bfb7a3e573fc8
ocaml(Constr) = 296ec0ed27566c6179008e82db07742f
ocaml(Flags) = e49471b92ae7483eb9df014819be4534
ocaml(Buffer) = 3bd1af04573ce2da7fc3dc04403e852e
ocaml(Pcoq) = 0df6270bbedb694ee0985aad2c136008
ocaml(RemoteCounter) = 6d0d3cfadd4e80cfc6e2aae1692a8266
ocaml(Reduction) = 921b78d873fb9f76fb50d1394378ead0
ocaml(Hashcons) = ad9b73f2e6afc3140ae037133e38a7cb
ocaml(Term) = 6ccf4b4190f0e13677c204b1fcf83412
ocaml(Dumpglob) = 6b7a61fbc55dfbf1ae37fb745dfaf5b1
libc.so.6(GLIBC_2.2.5)(64bit)
ocaml(Feedback) = 8e8062b8dfdf3dcf09672d5aa0ad4c60
ocaml(Proofview_monad) = f95fcc47ed3cc0968e0797b8a717f560
ocaml(Globnames) = 679a7df73bb86f8f5f612d00429ea5d3
ocaml(Option) = a7b6074830eff9488ce1e1d177ab90c9
ocaml(Misctypes) = 29aad8488348c9e3a27c3f1610f8f9e8
ocaml(Nativelambda) = 8e7ad07f2fd535a72ef72f838b8ea518
flocq
ocaml(Autorewrite) = b7c8c15080b2ba6649601b6a189a6dcb
gappa
ocaml(IStream) = b0c941aba53f2662e8e21874c7c472ed
ocaml(Impargs) = 4439d433c75b60cd645f87481dbc1db8
ocaml(Nametab) = c523403140474909d133da8fc45f7db2
rpmlib(CompressedFileNames) <= 3.0.4-1
ocaml(Gramext) = 7c243720c6c27ac52a3c41ec4af26136
ocaml(Bigint) = 3d35042ef46d760984c828e9000e9290
ocaml(Hints) = b7990aeb11853da860eb1bd8eaf27de2
ocaml(Retroknowledge) = d01dbfb976bfbf65fb43c6b6dab79c8f
ocaml(Cbytecodes) = 5feac8ee819a6f28644fe811208ac960
ocaml(Int) = 0d534c5053aa61e0398c4c6b8798f70d
ocaml(Univ) = b5e96974893eb148944c56ebecf9ae64
ocaml(Evd) = 0227a84e3af2e6601c975f8410a587e4
ocaml(Unionfind) = 22bf05097fd11e92c9b7504b5965c1f4
ocaml(CamlinternalFormatBasics) = 9642e3ed163e46770985ca668738ed5f
ocaml(Pervasives) = 999b28e3b7638771c87eebf5a8325e42
ocaml(Smartlocate) = 248a91616fa12ee581b37e742a698447
ocaml(Locusops) = 191893f7b515ab3e80a22bb504c1955a
ocaml(Type_errors) = 29968d04e55e2aaae3308d41e8a9c32c
ocaml(Store) = eb5ff9f57c88fb50607de4c6f49c75ae
ocaml(Decl_kinds) = 462493f97eb7721a889457b53d3b4ef3
ocaml(Str) = fc4cd9c73967ba1a8bc6360b21cf5f3a
ocaml(Declarations) = a248dc8324d2b45be469d54836fa19a2
ocaml(Rtree) = f49ac2e32474e1850daf2c754bf466d3
ocaml(Xml_datatype) = eff809db921c51e0795a4d3e61062072
ocaml(CamlinternalLazy) = 6f25aad2ca689d32011c428fb8260231
ocaml(Obj) = bff9812925bc903e1896c82e123d0a17
ocaml(Conv_oracle) = a8f3121fbd3c73d9cea800fa4d69590a
ocaml(Pre_env) = e120f27074dea9eefa9c6aa5255d1403
ocaml(Metasyntax) = 9e5138aa63adebcc22422375a0714faa
ocaml(Classes) = 26e82e1d8c6830ae7d9df815e2199ce8
ocaml(CMap) = 4b71fae31a26e7291479a8291debaa5a
ocaml(Plexing) = 7779eede1b67f76abef54d0650bf1cb6
ocaml(Redexpr) = 1127fdd25804befcb0bb73a87e68c182
ocaml(Genredexpr) = 338493e0c487adbd8669d2a99c504bf8
ocaml(Bytes) = 6dc691300ced97c0e319cbcc0a715044
ocaml(Hook) = 841244dfcdb29762d9a5f73a89dd409d
ocaml(G_vernac) = 45c56f24969d203bb375c5318631838a
ocaml(Locus) = 88592b35b5c930eb2a18f34220356d64
ocaml(Obligations) = 08d3a052d677cf34a57db61ec3e9959e
ocaml(Elim) = 2244f8cefed78d337d5307d6be4dfe05
ocaml(Set) = a16cc25d9afe91eb22559bef41e9ee28
ocaml(Coqinit) = 0887e23556884e74fc627c381a1a4b3a
ocaml(Genintern) = 97f0a3587bb9af6db5fb051c205d63cb
ocaml(Classops) = 21736fe000e70f782c409549b17000a1
ocaml(CClosure) = 662bb4b40a93d448e112a5535f2b2169
ocaml(Monad) = 2013cb45f8a0a21922c4c56d6206b75b
ocaml(Nativeinstr) = 28093ca729bbbb5281b61651c59601b6
ocaml(Evar) = b20b6e044349a7053ae46adb761c6d0f
ocaml(Pputils) = f4e4deae657df96a5895eee8964a3663
ocaml(Proof) = 3babfb1967025ea251d79ae9cef188ed
ocaml(Pretyping) = e7fcd3a0a3a01afedb490427af38ecf9
ocaml(Glob_term) = b46227c2af207e67b266f9ec730aa9a1
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
ocaml(Predicate) = 044835f939d5eb1963ec7f133d5e1f48
ocaml(Geninterp) = 9bd08ee8f50ab47195de2c280a1b7df5
ocaml(Sys) = c9608ce7bf745054a217110dcaac126e
ocaml(CSig) = 85b4cde1c53ad0a19217ac2219fcdf63
ocaml(Ppconstr) = 054a526f14ad01437ea4111237066402
ocaml(CErrors) = 4de5a1720167ce6369f0e4b6eca11169
ocaml(Cooking) = 530d38b00ed5e9f387362149e8c51aeb
ocaml(CList) = 60825e3a8a460a450c9bbbbb1f361a4c
ocaml(Lazy) = b2e565a5cdbd351dc15bc9061d30c458
ocaml(Tacticals) = 767018c63a3a734cc775a4bed0a3101d
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