SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

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

Name : gappalib-coq
Version : 1.2.0 Vendor : Fedora Project
Release : 1.fc23 Date : 2015-10-15 06:52:47
Group : Unspecified Source RPM : gappalib-coq-1.2.0-1.fc23.src.rpm
Size : 2.15 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/23/x86_64/g

Content of RPM  Changelog  Provides Requires

Download
ftp.icm.edu.pl  gappalib-coq-1.2.0-1.fc23.x86_64.rpm
     

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

Requires :
coq(x86-64) = 8.4pl6
flocq
gappa
libc.so.6()(64bit)
libc.so.6(GLIBC_2.2.5)(64bit)
ocaml(Array) = ae800d8cf9903f1d36856950940430e6
ocaml(Assumptions) = 16020e8186984b7edcdb4f474614611e
ocaml(Bigint) = b2098b33e959abbdeb712ae2a55e8e48
ocaml(Buffer) = a579f4a57e300ec755f84af883c1e51b
ocaml(CamlinternalFormatBasics) = 8b069fca1e4d9316b588e5554f38bb24
ocaml(Cases) = bcd5121150a4bd1c7507c40007bd930e
ocaml(Cbytecodes) = c8b6d39a5dbb35c6dc847dcca89eafab
ocaml(Cemitcodes) = c7e8672a44cac018ca0c5a2c7fd0d1e3
ocaml(Classops) = f5f5ef316e600c61ea47df60ee3023cc
ocaml(Clenv) = f8c902f133a71e03c68426b8ecba8c40
ocaml(Closure) = d97830af39a57ce5bdfbd055f37b4969
ocaml(Coercion) = bb52b7e40a2b179a130ce31ffd21ba3a
ocaml(Compat) = de2c81ddd1168986f95007fa6820e946
ocaml(Constrintern) = 2c46531b766fc8dc1d8c2759808f9f3d
ocaml(Conv_oracle) = c025e048f8a2b554bd63f50338dcd8e8
ocaml(Cooking) = 5dfa62b9f2d3660f3a33c2bc7c354c66
ocaml(Coqlib) = 6ad67569ff9bd96483a95f99e77b8ecd
ocaml(Decl_kinds) = 588b0ba55cdfbc95e38a12bacff76839
ocaml(Declarations) = a06385b4b596dab1c07a21862fba2857
ocaml(Declaremods) = fef954e9654c6c10016ffc0ece1366f9
ocaml(Digest) = eab54f58b34b8a6fdc763db6966614a1
ocaml(Dumpglob) = 42475cf7b0df3305ecfdee1f5c04fa2b
ocaml(Dyn) = 5a9ee2020253d5f056484830798a9cf2
ocaml(Egrammar) = fb2468b2078e2a285666782790064929
ocaml(Entries) = d426f4856b967b933d39335dc6cc3210
ocaml(Environ) = f6024d78293beda9d986d17e0da26ac3
ocaml(Errors) = 530a290394d6541675c5394a398156cb
ocaml(Esubst) = 118cd41e3321be6c23464f0421d6ad4f
ocaml(Evar_refiner) = 733c3fecf8dbe4f164df039577885ffb
ocaml(Evarutil) = 917273a59f14ce1476020011ac88530e
ocaml(Evd) = ecd9f72e46c1843ca5a1c6889764f38d
ocaml(Extend) = d6ae46bc1f669c4da53d9ff1cccd5c25
ocaml(Filename) = 3817bec1dad20c6f594d3a85b13020b8
ocaml(Flags) = 2def628aca984192dcc400d1e9100bee
ocaml(Format) = 61d4350242b30078d3ad96c904c9f7a1
ocaml(Fstream) = c42798e38353055be90f4363e7eb611a
ocaml(Genarg) = abef2a8e2188a59443fd84c46c029aa1
ocaml(Glob_term) = 3a3f13dddc99452d63ebdc240cd7c048
ocaml(Gmap) = 0c2f931a72be00904c6f1449d70668e9
ocaml(Goal) = ff94e7f65bcc8ea8571d7e115836669e
ocaml(Goptions) = ff0bcd5ebbcbb87ec0e8b1dab7f60af0
ocaml(Goptionstyp) = 2ff996e3a3fdebec23bcd97d0d75f878
ocaml(Gramext) = 1ff7584490ae7a3bd5500e4b376d7833
ocaml(Grammar) = 929eb67258df2011211f99bb4881c775
ocaml(Hashtbl) = bb8e269d690301a1c4ff14a08e96e83e
ocaml(Impargs) = 9d997524cc9e3c751d9ca5a4b0f067df
ocaml(Inductiveops) = 1626c6a559bc3a7a20be25a9eff59dbe
ocaml(Int32) = f43b8a2972804b40e28b661b6fdf157a
ocaml(Lazy) = 7dba0bf02f60e5ff44e9e4057263f28d
ocaml(Lexer) = 9e78ff54b199ee9596f5f4a1b02b4c23
ocaml(Lexing) = 1be6a5484fb3cfb69d2c981438a7be62
ocaml(Lib) = 6a5acbc374634ed73cff5a86c46e6c30
ocaml(Libnames) = 27309ad618c8413f27807a3598648d62
ocaml(Libobject) = bdb04cc2de01d3f69bf5740314202b7b
ocaml(List) = 8988208489274193e4e3f69dc6ec2f75
ocaml(Logic) = 2561cd67ad0e1a0e75f305e81e6fac70
ocaml(MLast) = c74b5aaa1b21777164adc6d1f0816c91
ocaml(Map) = 770e6123e5460eeb42d3050f13c5ad53
ocaml(Mod_subst) = 2e80c47046d6d76019590cda965e86ab
ocaml(Names) = 86925d47691d1a9604cf63c62c0a6431
ocaml(Nametab) = 49aa048bf9c2cfbcc69716676666b0aa
ocaml(Notation) = d797633f34029951e82adf9db38767f9
ocaml(Obj) = 8b014ec57a472d9f3922b63e5de9d1f2
ocaml(Option) = 04c29715faee30df3eacec90f7704860
ocaml(Pattern) = b059883f9146e64dd6eafca71270df7d
ocaml(Pcoq) = 7a85ea39e9214847ff7ef9f5a8107c4e
ocaml(Pervasives) = 0d015a5a2136659b0de431be7f1545be
ocaml(Plexing) = ae4665d54a72287d155582ef999f4bae
ocaml(Ploc) = 768131dba7501a48dc6124328d0fd65f
ocaml(Pp) = 214bb70159506dd4b6d64ea91de80830
ocaml(Pp_control) = 04740a815d7e2cad09ef32df65068876
ocaml(Ppextend) = 52f6d4a8e2b46d8c235460a04c9eca2c
ocaml(Pptactic) = a2bcfac07c16e6316b69de21aad6a01c
ocaml(Pre_env) = 129816eefc0c9dd30c1c368852dba614
ocaml(Predicate) = 0a1ed287e6cb5e4fdd29ee90f4d251b4
ocaml(Pretyping) = 696ac697687dfc60e35f73f45183cf68
ocaml(Printer) = 3e824c5193607ad4e97c3fbc90698d59
ocaml(Proof_type) = 56913c3490e18b423833f1468aaa3839
ocaml(Redexpr) = be39e4d17e10c9e3bcbb3fb2b51c1b72
ocaml(Reduction) = 933c4494174fc715b356ccabd0167e76
ocaml(Reductionops) = d69e94e86ea46ef3c8bb0c83565b18c6
ocaml(Refiner) = 380698de4b06d0eb963dad89fa7e05a4
ocaml(Retroknowledge) = 14ab026ec954ef98f89f8c29d3476cf8
ocaml(Rtree) = 6911f2beb6701dc499044ba7937f8b54
ocaml(Safe_typing) = c3e3dae7928ad826d3c6cb8fea316332
ocaml(Set) = 487197ccd2fea64d52f1cd917061caf2
ocaml(Sign) = 7d16d9f57f9550d69de709d88f08043e
ocaml(Store) = 1cfac1889819e91867bfbb643edd41cc
ocaml(Stream) = 55948988e71c3ee1749feb21ccec9fc9
ocaml(String) = 9cb286f2c4569fd32c379b1a05c7b590
ocaml(Summary) = db9841087c9200171c75d21695867557
ocaml(Sys) = 0ce699458ce4430954d7e6a78874647c
ocaml(Tacexpr) = dc96178a773b48e65f569321b65385a4
ocaml(Tacinterp) = 96eec422cd323b2b54b5ac303cd0f7c2
ocaml(Tacmach) = 0eaa4ea91ad849dff2bb04d82aaa8eb8
ocaml(Tacred) = d1f054255661e5a30245b25e31a5d26f
ocaml(Tactic_debug) = f4660df60c01cbddbe6584d578935376
ocaml(Tacticals) = 38dbd5ff9bc075322fa29be3991e4efd
ocaml(Tactics) = 42024c9a1323aa399713ff3979f27cc5
ocaml(Term) = 3d9a3f28d2fbbb8e5c1e8ff2c7e3c939
ocaml(Termops) = 3b00c10e40548f1bb32cefd70923737e
ocaml(Tok) = 39ebeafe54a3f28ce525a95db111e46a
ocaml(Topconstr) = bd2d7bca878e20c34835832c6ea77bd4
ocaml(Type_errors) = 603ea5c8e4223551c880c82cc0cab202
ocaml(Typeclasses) = 67e9963a3da7d164a44c29c3bc4b6264
ocaml(Unification) = eeae2f526540eb93a72bb12ccb41aee7
ocaml(Univ) = 5bedd196ec4778302aaabe6ec5225c05
ocaml(Util) = 555b1986d20d7f70439def1828ef4355
ocaml(Vernacexpr) = d06a83c276ce1d3a0fa428315c412cb7
ocaml(runtime) = 4.02.2
rpmlib(CompressedFileNames) <= 3.0.4-1
rpmlib(FileDigests) <= 4.6.0-1
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
rpmlib(PayloadIsXz) <= 5.2-1
rtld(GNU_HASH)


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

 
ICM