SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

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

Name : gappalib-coq
Version : 1.0.0 Vendor : Fedora Project
Release : 8.fc20 Date : 2014-06-16 22:22:57
Group : Applications/Engineering Source RPM : gappalib-coq-1.0.0-8.fc20.src.rpm
Size : 2.20 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: /packages/linux-pbone/archive.fedoraproject.org/fedora/linux/updates/20/x86_64

Content of RPM  Changelog  Provides Requires

Download
ftp.icm.edu.pl  gappalib-coq-1.0.0-8.fc20.x86_64.rpm
     

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

Requires :
ocaml(Safe_typing) = dc7021f1276d86c8c5a6a7dd9e98dcc7
ocaml(Lib) = 6057de67264e0704433bfbe4f9586c2a
ocaml(Cases) = 77fdec840aed0dedebd6d4122db0bd1b
ocaml(Rtree) = 98fccc81d0427129c4c836b2f008fd50
ocaml(Int32) = 265928798c0b8a63fa48cf9ac202f0ce
ocaml(Typeclasses) = 7e56e403e31ebb85b87b1565ab716ba6
ocaml(Summary) = 323a056a2aaade2727882042108efc19
ocaml(Logic) = 93b71ceb2843cd792c954dc9deed75ed
ocaml(Fstream) = 630a8a34ff89dff6d1290c4b41ba4fd5
rtld(GNU_HASH)
ocaml(Pretyping) = cad1d197bdd6056126781d5dcdc4ef07
ocaml(Predicate) = 004e109f6057a785bf21b1bfa78509ac
ocaml(Dumpglob) = 793788a63283857b78bbb078c4669bf1
ocaml(Flags) = 4dd236be4354d07ced2ae7f5ed2863df
ocaml(Egrammar) = bb8a7ed5c526eed06dd920153113364f
ocaml(runtime) = 4.00.1
ocaml(Store) = 416cf0db66fc749a2c833f3cfe9bdeed
ocaml(Lexer) = 89fa97f58b73f88b544be9ffad139757
ocaml(Glob_term) = 1e222126e708b9495c6873cecef07653
ocaml(Lazy) = be13470d54bbba2080e16d4f864ec34b
ocaml(Pre_env) = 54b70e5987e9971bf18070493b281894
ocaml(Pp) = 00ab85d22133ac5a78fd8c1e0f999ad1
ocaml(Conv_oracle) = 0bb785400b32024678d21d12a80da9aa
ocaml(Pervasives) = 4836c254f0eacad92fbf67abc525fdda
ocaml(Obj) = ad977b422bbde52cd6cd3b9d04d71db1
ocaml(String) = 54ba2685e6ed154753718e9c8becb28b
ocaml(Retroknowledge) = a06579b2a147ec5f6152fbafab993c41
ocaml(Lexing) = 7e306603bdda9b5b4c50d1aac8def12a
ocaml(Extend) = 098bd04793dd65d34671e6d7da987e96
ocaml(Buffer) = 3f6c994721573c9f8b5411e6824249f4
ocaml(Hashtbl) = 718cd6ce8bc18371ce22483e362f78b4
ocaml(Gramext) = 4b4437e57950e99cbf7712292ef87351
ocaml(Environ) = 14c4a2b809facdca0e66b5257f143711
ocaml(Libnames) = f8ebb7814efd6bb6332be1dd356b6c58
ocaml(Evd) = cade96b363d91e93dbe4bd0f2a0da4c3
ocaml(Term) = 23791a837629414d61eaacbed14cb49f
ocaml(Vernacexpr) = eb60b9b13adf7eaf9b7cfb5bf336aad2
ocaml(Ppextend) = d132512d969ebbbf147e384beae768c0
coq(x86-64) = 8.4pl4
ocaml(Cbytecodes) = 7199c9e5af1b3e17fb385d61a0e239ed
ocaml(Proof_type) = 7dff61b4a723c06219439e82798db667
ocaml(Cooking) = 41459ea8b491ab8811b24af37abd650a
libc.so.6(GLIBC_2.2.5)(64bit)
ocaml(Tacred) = 433d5cad3dcb2527bdd2b506a0df7e36
ocaml(Util) = 2c8636a90647500f92f50f2cd9580c73
ocaml(Digest) = fc1ddbe7729c06f1551c4154795b3b6c
ocaml(Tacexpr) = 5219bdd8abe15310f75a33dddf7381db
ocaml(Redexpr) = d43bdaae3b57e54c39e0b8958ea0df88
ocaml(Errors) = e0c71de8e91fc9cf310e3e6a19388b1d
ocaml(Refiner) = c092d4a65c681693529c14b9efcefe3a
ocaml(Notation) = 35ad7b9c7e84f753b828810c87a062ce
ocaml(Tactic_debug) = 3555fe5c3f8b0daf25604e94c3368a76
ocaml(Dyn) = 5268a7911e5e911ad71a17ccc349e047
flocq
ocaml(Reductionops) = ef77d1ab37ff058220387b14f29a576a
gappa
rpmlib(FileDigests) <= 4.6.0-1
rpmlib(CompressedFileNames) <= 3.0.4-1
ocaml(Mod_subst) = 0509d33a8b8b2a667a067dff40a75d77
ocaml(Option) = 66fbeb921db79ae9d101e58c722194d6
ocaml(Grammar) = 67b180ea66b3e2c92b89fc0611d675d5
ocaml(Set) = a7bdd82abd2a5609c0242e51ef43cacb
ocaml(Sign) = 4aef2f214d89a9be5cc3e0ba30f0cd4e
ocaml(Tactics) = 949c2c75396c45ddad9a28f3e8495e7d
ocaml(Classops) = 062ff3a5498ac45fd56f05078c50150c
ocaml(Entries) = 9cc07671b7dcda030056c1ddda5bf7df
ocaml(CamlinternalLazy) = 7e4f61f0abc0dc4bb87447429adcf88a
ocaml(Tacinterp) = bab8504a355b8a04c2e353880ab9d0c2
ocaml(Reduction) = 7ea4c7a1d9cdc88fc3aab5d2172a8806
ocaml(Names) = b47523c48b8dbc2b6f9287ac9f2a81ea
ocaml(Filename) = db19aeb2a8d7e9bd0f4c54d51c6a433e
ocaml(Coercion) = 7d6a142f1f8cbbec9c0bf1d440187e09
ocaml(Type_errors) = b2f9fb9e63c1d0b3f0f277b9d84d47bf
ocaml(Tacticals) = 94cc097d8189ebd8f96d667b544cdfcb
libc.so.6()(64bit)
ocaml(Printer) = 7f140ba9188ec54ff4f0f295b7ed61d6
ocaml(Nametab) = b313970a0cd0c996044e77b1d6df3a21
ocaml(Pcoq) = 9b2dc03adce5ae19b52efeecd4c4f738
ocaml(Array) = 4d5efba91ec70acd7b184fd4b277708c
ocaml(Gmap) = da81102e899bdd54bc951914c692cf8a
ocaml(Pptactic) = 74dbc86fe99bf9279f6615abf0ed95e1
ocaml(Compat) = 5af19461b834ba821828839886984648
ocaml(Goptions) = c3e32f01042357a288252000feb434e7
ocaml(Topconstr) = 526b9a8879cef3314d03d1a840cbfa3a
ocaml(Format) = 6e6b7b75c544ef4ca673a763aec805af
ocaml(Pattern) = d6667ce0c1d75cc1fc8ce37512c0af0b
ocaml(Plexing) = ed09962042e18e13fa65ce7663d03089
ocaml(Constrintern) = ab94d8c79ee2e220d6a6eb93ec10ab46
ocaml(Coqlib) = 113ce647f691e7f07c295f48049815e4
ocaml(Inductiveops) = 4253b2b3e0dcc893d701c7a4400506db
ocaml(Genarg) = 851f8eeec00eea6058946371f73c7a22
ocaml(Stream) = 85d259e9a37648998b6c03b551d68e46
ocaml(Declaremods) = 170f5d74e77f011480a294aae30c6391
ocaml(Ploc) = c49f559126440f76caa25c12c166b110
rpmlib(PayloadIsXz) <= 5.2-1
ocaml(Termops) = 7dfd13516290ef7621ab5de60db9dee0
ocaml(Cemitcodes) = fb3e3e759e50d99c41e6dc2dc3ec7b22
ocaml(Impargs) = 25f85d5dd2cbfab62b34913e8260ec2b
ocaml(Evar_refiner) = b97d89dde1c7897d06765e921b9b660e
ocaml(Sys) = 45d17525db422614c1cc84b2d9f27926
ocaml(Pp_control) = 78093873beb4b6ebe4c8463e11948248
ocaml(List) = bd7c662c09e850306a62c12fed5ef5ce
ocaml(Closure) = 7217ddb8f661bcdea39f8f1f65520b2c
ocaml(Esubst) = 8f64f3122ff9d3fbfffe8c86edd3ac91
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
ocaml(Univ) = 4d51cbe0d84559fca901901a8f95b467
ocaml(Clenv) = d7ac4fe646b0f6512c1574bf6084dec6
ocaml(Assumptions) = 6b5ca01318306dd74a24a9476fffd199
ocaml(Evarutil) = 84fa8b4ecc14b725bfd549b949fd0439
ocaml(Map) = 1be6bb7484ad2000575776b38d423f2f
ocaml(Tacmach) = a9c00900c50236c6877f65159de53df4
ocaml(Bigint) = d8a4f2c6a6c291028c11148572c27c15
ocaml(Decl_kinds) = 4c63a4e179d045666b661d798110f392
ocaml(Goal) = a4bb3cb06b501cdb4db7da9f06b3e994
ocaml(Unification) = 2d3fef08e39111359b241f3ea23796c6
ocaml(Tok) = 588f401b33b9cd2284108b2f04a1ee0d
ocaml(Declarations) = 7cdd4235558a50e3ab9c127652363b0c
ocaml(Libobject) = eb3782a8bac828422880c4898c231ff3
ocaml(MLast) = 8517b79e346c2ff18174da6c180fcd26
ocaml(Goptionstyp) = bf3ac8b37058ca85449f5106e12c9558


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/gappalib-coq
/usr/share/doc/gappalib-coq/AUTHORS
/usr/share/doc/gappalib-coq/COPYING
/usr/share/doc/gappalib-coq/NEWS
/usr/share/doc/gappalib-coq/README

 
ICM