SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

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

Name : gappalib-coq
Version : 1.3.0 Vendor : obs://build_opensuse_org/home:lorenz
Release : 7.3 Date : 2017-01-18 20:49:39
Group : Productivity/Scientific/Math Source RPM : gappalib-coq-1.3.0-7.3.src.rpm
Size : 2.32 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:/lorenz:/formal/openSUSE_42.1/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(Constrintern) = 457f296783198bcda8f2e21a125b652b
ocaml(Impargs) = 580558ee3469b2549a6a49dd1b50857a
ocaml(Hashtbl) = bb8e269d690301a1c4ff14a08e96e83e
ocaml(Type_errors) = 5ec63bb5796ee49580af6c347e6160a9
ocaml(Retroknowledge) = 373259673499e9a19e8b0464142293ce
ocaml(Extend) = cac3bdd30907fc358cd368f5faf5e801
ocaml(Hook) = cf229f2840d665552befb6267baeec8b
ocaml(Cooking) = 3f298a07769d6d3804ceb3442512dcdd
ocaml(Printer) = ed08d9dd08c2c9b7eb120bcd03930eaa
ocaml(Int) = d84ea2cc68f92c774ecdb69fbd33aa72
ocaml(Predicate) = 0a1ed287e6cb5e4fdd29ee90f4d251b4
ocaml(String) = 9cb286f2c4569fd32c379b1a05c7b590
ocaml(RemoteCounter) = 50daf91cb3a0aff06eb5380d78853317
ocaml(Dyn) = cd55621df184249c4c36d88947398c29
ocaml(Unification) = a5e8d741d1e04bbb4b6d37bda99ea423
ocaml(Proofview) = c2918647ed17478fa5202c03daef1fa7
ocaml(CArray) = 6e4a42f02ef3c429ac82a769d146eed6
ocaml(Pattern) = 0efc3d1efab8a712fe6d911dc2859d66
ocaml(Tacexpr) = 52d73a06c30f92e12ae13c965c3dbd6f
ocaml(Ploc) = 768131dba7501a48dc6124328d0fd65f
ocaml(Tacticals) = de29d436661e75be406936d3f6d5af8e
ocaml(CString) = 0393355359613bdfbe318e23c0c487cb
coq
ocaml(Environ) = 7cd36135f65465e51ce09cb25fa4434b
ocaml(Compat) = bc030bf42994dbaecad8c70780396694
ocaml(Esubst) = 69af2a8ccd4ee95b70163f61ca344ea1
ocaml(Tactics) = 0aeb805b9fa5d02ac1046bde950c8b71
rpmlib(PayloadIsLzma) <= 4.4.6-1
ocaml(Logic_monad) = b66af15d0fb7c948eb986c142211e206
ocaml(Buffer) = a579f4a57e300ec755f84af883c1e51b
ocaml(Proofview_monad) = 4f5d1822f783d79374ef647293847332
ocaml(Format) = 61d4350242b30078d3ad96c904c9f7a1
ocaml(Flags) = 7136212ada32dc23869eedf4dbe613ef
ocaml(Constrexpr) = 58a6b0cb769b2a69b205a5fb6123e93a
ocaml(Nativelambda) = 23578b02d214a147b5b7c8a0d9cefbdc
ocaml(Obj) = 8b014ec57a472d9f3922b63e5de9d1f2
libc.so.6()(64bit)
ocaml(List) = 8988208489274193e4e3f69dc6ec2f75
ocaml(Constr) = 2f9a4731baed8d97261d2878c2ea5695
ocaml(Declarations) = 375428fef9df0e676b23dd52b8847227
ocaml(Mod_subst) = fc1bf36ecf01f70531bba5b529153fa8
ocaml(Digest) = eab54f58b34b8a6fdc763db6966614a1
ocaml(Goptions) = 0f0ab09a6f5e6e58661c2be30fa4410e
ocaml(Hashset) = a81683b978c41b71114faac07c58b84b
ocaml(Set) = 487197ccd2fea64d52f1cd917061caf2
ocaml(Bigint) = b2098b33e959abbdeb712ae2a55e8e48
ocaml(Pp) = ef108c5fcc84ef75009f47319600b383
ocaml(Util) = ad25ab575d6a9982f5689646671e71c1
ocaml(Lexing) = 1be6a5484fb3cfb69d2c981438a7be62
ocaml(Tacenv) = 7bff996cc4d2c0c1e6ab284a9388aca9
ocaml(Evd) = f37ad891d2ed6037b72ecd19ee0ecc07
ocaml(Genarg) = 04886733fc3674e646498211fff8edc8
ocaml(Pervasives) = 0d015a5a2136659b0de431be7f1545be
ocaml(Evar) = 0af80407b095156978ccd3442698c726
ocaml(Xml_datatype) = c8b4737e8b2c382cff5d0e5ed37ca089
ocaml(Pcoq) = 962f3a07e863f5ceb32b4ecde384eeee
ocaml(runtime) = 4.02.3
ocaml(Plexing) = ae4665d54a72287d155582ef999f4bae
ocaml(Pretyping) = cfafdeee906cbf78497c80915d2f3992
ocaml(Errors) = 492b1fab2753d750503b1fd551bc31a7
ocaml(Proof_type) = cb35f259615b990c60e386c0b9c3c896
ocaml(Uint31) = 751404b523ace727aad47be62a3e0064
ocaml(Map) = 770e6123e5460eeb42d3050f13c5ad53
ocaml(Redexpr) = d2ba886de5c80641f0fadf7dbdd98275
ocaml(Tacred) = c52cbb91719da4471cadcf9c0c0b1510
ocaml(CMap) = adae6dc727e81ae69789a2a9ae6d7e77
ocaml(Misctypes) = f8cb5d7b8717a4ecdec2c404d461404a
ocaml(Geninterp) = cbf7aeff0509db0b96366a50ab99e99e
ocaml(Grammar) = 929eb67258df2011211f99bb4881c775
ocaml(Reduction) = 3154f4a47f95782569c7f4be2f7ab02b
ocaml(Coqlib) = 5897c6671fd18cf4d525f8a3a9f8850c
ocaml(CList) = 681938883c54cfbe68bca5f0a7e9dfa8
ocaml(Gramext) = 1ff7584490ae7a3bd5500e4b376d7833
ocaml(Stream) = 55948988e71c3ee1749feb21ccec9fc9
ocaml(Vernacexpr) = 9c2c871541f216931f038bc6af30e5be
ocaml(Proof) = b68926c50fd775c8806cbe6ea6f8a669
ocaml(Evar_kinds) = 78b73c4496e7b114665824891fe804cd
ocaml(Closure) = 6b6fe8a018cc1ab420ddccec977c3181
ocaml(Names) = 5db8ca8d37c14e91e2d61b80c2d8b4be
ocaml(Pre_env) = 9d3ff130fc8bc787059158ef8c761e00
ocaml(Lexer) = 80ae1cec3d3cc5e8ea872dfe928c8222
ocaml(Feedback) = 208321e0d1391d4b777fe53df6225211
ocaml(Reductionops) = 0a8f903410466a4e1c96b7c06f38dd52
ocaml(CSig) = 1c57a3b2223ac716e5ecfea99243e022
ocaml(Genredexpr) = 30021b47efd7f7eaaedcf065d35e65a6
ocaml(Notation) = 84993daedd889f8c5d58a4d12ce6297b
ocaml(Ppextend) = 81adeb8605b1504a5fc68e8f6c9b63b5
ocaml(Nativevalues) = d044ccd4f986125d6074b3f450b1f357
ocaml(Universes) = 814e2e802955038d50942df000c2ae72
ocaml(CStack) = 920cdd9278656c3a99b9099aa5086825
ocaml(Evarutil) = c1060abf6c798e15171b4480ffc6b127
ocaml(Globnames) = d4e44631f07ab4beb5b33201a4ba3e8d
ocaml(CSet) = ebb037bed49b6df2d5f2665e9da9e87f
ocaml(MLast) = c74b5aaa1b21777164adc6d1f0816c91
libc.so.6(GLIBC_2.2.5)(64bit)
ocaml(Unionfind) = ca042e7789c0e04de5fb99972a6aae6b
ocaml(Monad) = 227ade805f5593887710ad03a0dce175
ocaml(Nativecode) = a381280158f19f1b0a2438b241f5c3df
ocaml(Hashcons) = 93eb1e0d2155cb5e7089aa95441d2325
ocaml(Safe_typing) = 3be07db96880c2fc05064debf1ea90dc
ocaml(Sys) = 0ce699458ce4430954d7e6a78874647c
flocq
ocaml(Cbytecodes) = 4fa3928cb765073ebd7c8f9712f269b6
gappa
ocaml(Lazy) = 7dba0bf02f60e5ff44e9e4057263f28d
rpmlib(CompressedFileNames) <= 3.0.4-1
ocaml(Future) = ec253b746839aa424c1394de93875d77
ocaml(Exninfo) = 7cfd20a2a9389edaa98dadacc7eaef11
ocaml(Nativeinstr) = f4cb723b061f6cbbde56793ebbe438ac
ocaml(Decl_kinds) = c98097ade10179945fcb61785c2bf8f2
ocaml(Term) = d9596979d7cbf34e263a815af800178c
ocaml(Nametab) = 630511b38afbb47e7048c47936e33088
ocaml(Store) = b6b252f5e18ae78a3c874776d24a3380
ocaml(Vars) = 5965dd216698e0760cc04e44f6ba2105
ocaml(Sorts) = 96c173aa0db6c8deb5f1d44d32986e92
ocaml(Tacmach) = 9fab54a6ff09587b1ee2ac52a6c2af61
ocaml(Token) = 411e4d92b7830d0f72be80710575d9e2
ocaml(Clenv) = 1b7e0dd60334da029dd99430b7280152
ocaml(Mltop) = 3860cf6eb5e61deadbdb189a3393eddc
ocaml(Rtree) = 176222c27a80fb87459e80ee2c8aef43
ocaml(Glob_term) = dc5ce589a38f60457e2673a76bb9bb16
ocaml(Univ) = 273f281ed7d948700a535377d5ea4992
ocaml(Stateid) = 6285e5fb867d9583be67b9f69d9ed2ac
ocaml(Array) = ae800d8cf9903f1d36856950940430e6
ocaml(Int32) = f43b8a2972804b40e28b661b6fdf157a
ocaml(CEphemeron) = 42b91c50de5d0145d4713ea4eeb99c13
ocaml(Str) = 98bc31cc4150a0a7e1fa3ceb656e6da5
ocaml(Libnames) = 38355309c5882ab176cf801a2420d350
ocaml(Fstream) = c42798e38353055be90f4363e7eb611a
ocaml(Tok) = 1df9abff2be68472d10d470768a07336
ocaml(Locus) = 2eacaad8ff093471f8fc18120b828561
ocaml(Primitives) = a3553f78791523a79bf3bcdf80c20618
ocaml(CamlinternalFormatBasics) = 8b069fca1e4d9316b588e5554f38bb24
ocaml(Opaqueproof) = 47d29b2efd9fd6ad977eb69b0dd9811a
ocaml(Cemitcodes) = 85f7f2bee725d295074aeaa676991dd8
ocaml(Loc) = 4e04ac3aaa70862b644e19145393cfc7
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
ocaml(Goal) = 3145e011444841d9d4659e0561167685
ocaml(Notation_term) = 6da03d311be4b80b14aa0b307d13afab
ocaml(Entries) = 3406c4debef13de3912e5fa7dea25e87
ocaml(Conv_oracle) = 1356162cd5e00b78bb23306ae871c8ce
ocaml(Context) = c95ba4f740028bf612861f288b6391f4
ocaml(Dumpglob) = d7accc1878042d9aec16a3871bb59f51
ocaml(CamlinternalLazy) = 122717041759525de93c0247d8e18b5a
ocaml(Filename) = 3817bec1dad20c6f594d3a85b13020b8


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