SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

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

Name : gappalib-coq
Version : 0.18.0 Vendor : Fedora Project
Release : 1.fc17 Date : 2012-01-09 19:53:22
Group : Applications/Engineering Source RPM : gappalib-coq-0.18.0-1.fc17.src.rpm
Size : 1.57 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/releases/17/Everything/i386/os/Packages/g

Content of RPM  Changelog  Provides Requires

Download
ftp.icm.edu.pl  gappalib-coq-0.18.0-1.fc17.i686.rpm
     Search for other platforms
gappalib-coq-0.18.0-1.fc17.sparc.rpm
gappalib-coq-0.18.0-1.fc17.alpha.rpm
gappalib-coq-0.18.0-1.fc17.ppc.rpm
gappalib-coq-0.18.0-1.fc17.ia64.rpm
gappalib-coq-0.18.0-1.fc17.s390.rpm

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

Requires :
ocaml(Pattern) = 9e0ef1b114e47b93256c47cd53a866c8
ocaml(Option) = 0442e3e5203037a3eff12e730264ce9a
ocaml(Redexpr) = 38c4253305a6259c2839e023a19ec239
ocaml(Typeclasses) = 669a19ace94ee24c65b64f2be2f606ec
ocaml(Util) = 3fff17cfba1c46a9ee0500b731b2d418
ocaml(List) = 9c85fb419d52a8fd876c84784374e0cf
ocaml(Proof_type) = 7d1f8b216932f9f3d2d4b3c173ec91a4
ocaml(Notation) = eecb4e5de54e7837babd26f5a0c9d721
ocaml(Univ) = 2d2b9f5b7a2c0a2758eea57b59d54008
ocaml(Fstream) = 0638542c744443f2b176b95a5b211df9
ocaml(Type_errors) = 0b49356b65c8a55171a8b0c801ce2f92
ocaml(Extend) = 915c788d92f729998081e3e6e6e4ef0f
ocaml(Evd) = 79ff8abf6d0e9933be8ff0af7da36a8c
ocaml(Constrintern) = 88ee542ebf60767f7207d218e604757b
ocaml(Refiner) = 1b1c7e99281090f4e20946ec2f42d0da
coq(x86-32) = 8.3pl3
ocaml(Retroknowledge) = 74ab3e6ad7ea1dee3580e62a32e88324
ocaml(Lexing) = 7d5623c54d065ad3f652261d2776959c
ocaml(Pcoq) = 36c2b343d679594c95d4a67b4618a32c
ocaml(Environ) = 974eabe1a005a2ff38852ef473483954
ocaml(Term) = 4ab47137eedd146fbdd7fa73157b2c9b
ocaml(Extrawit) = dc8fd6ed763fdcb281da1dc2dad0b02a
ocaml(Array) = 720848e0b508273805ef38d884a57618
ocaml(Bigint) = a5fc4be04fd0ecb0f6ed15d8aafc4e1c
ocaml(runtime) = 3.12.1
ocaml(Coercion) = 29db113832e012f42dd8258561d642a0
ocaml(Pptactic) = d8b30bc970acbd6d9a29a97dad5b9421
ocaml(Ppextend) = b8787e38cf274eb84babf5dcd4b48190
ocaml(Decl_kinds) = 96712336ea86ab2d6478174b7dbbd7aa
ocaml(Plexing) = af03d74fdd25c7f5adef6fedca18c3f1
ocaml(Compat) = d7503031e2d20b5f766ac706c395b783
ocaml(Clenv) = 2f35c930a1bf227cd1855ef26901f754
ocaml(Stream) = cc2abcbdc5423e35862902ae0a0a4a7d
flocq
ocaml(Pp) = 25f853c186a203ba8122b07ca95589d0
gappa
ocaml(Closure) = 7c1099771b38c2bd2dfdb8398c2514dd
rpmlib(FileDigests) <= 4.6.0-1
rpmlib(CompressedFileNames) <= 3.0.4-1
ocaml(Printer) = 9c383c3f48c88335692749941eb7e818
ocaml(Map) = 971a915c5d6e79ba8c5a551e0767f582
ocaml(Unification) = 2fefe1310892fe7709ce617c1d451afc
ocaml(Token) = 1148e70ee439dfccb0930823a9dfa2ed
ocaml(Stdpp) = 4a9363c5c3c814dba55fb29c668cff31
ocaml(Libnames) = 940ebd6de65cc79d90d8d89d3a6ce3b6
ocaml(Set) = 7b178c9cf52b5cb8145441e1a0d309f5
ocaml(Hashtbl) = 9c86f7320512d6740a75017fd66156a8
ocaml(Tacinterp) = 277d766530346a33ba7f2de32d59ba9f
ocaml(Dyn) = 57a60f030b39bf0e026afe272276ab77
ocaml(Proof_trees) = c31aee9510a6d0f8101e02de4a641739
ocaml(Predicate) = 8b32cea1eab0d46cee1d01cc765ff771
ocaml(Flags) = 24caa56fb61169846604b56a994c62b1
ocaml(Obj) = 3aeb33d11433c95bb62053c65665eb76
ocaml(Pretyping) = 4158d04b76fd82d4e6af08e70d0468b9
ocaml(Cerrors) = 34a3233d7c187061bc9914af788a4ece
ocaml(Tacticals) = 199fde59acbc836b2b1ffd034d28a94c
ocaml(Termops) = 2bdff60abb1f2fb3f80e1ecc81f4dbcf
ocaml(Scanf) = d7b5d0c4bd7ca9e180f113cbb292e7f2
ocaml(Cemitcodes) = eed11d6b55a2f8e10b5e53f10febe7da
ocaml(Names) = a519db1ad3ac0dedf625bea9837003a4
ocaml(Cbytecodes) = c54b34663f061c25032c8f4f4c945863
ocaml(Lexer) = a57ea34559a7929e88ed326b2bfc65ee
ocaml(Buffer) = 40bf652f22a33a7cfa05ee1dd5e0d7e4
ocaml(Tacmach) = 937d63cee688a3c9f44f47a7f6f44f97
ocaml(Dumpglob) = f44d3636072a342edbfd849710b52969
ocaml(Gmap) = f152a391a85c939f97428e6aacc5fa0e
ocaml(Summary) = 8564a3500e9cd12c1132cf68df14d999
ocaml(Rawterm) = 1b21fb46a9b92b9446773fc2f5dc7a15
ocaml(Lib) = 8ab5dc0b1ba10c13dd3fef3512953ce9
ocaml(Tacred) = 76cb1df80d1e72e9a1d585b91bac1d31
ocaml(Reduction) = 2b87bd591d27185e51a23d93c9c90803
ocaml(Ploc) = 5379c25f9413f7df5d39ac3be287d946
ocaml(Gramext) = 5dd2e0bee1e8f1d4eae3e3c00e14cf54
rpmlib(PayloadIsXz) <= 5.2-1
ocaml(Pre_env) = a3022b845d28538bd52f334befd99e8b
ocaml(Int32) = c91c0bbb9f7670b10cdc0f2dcc57c5f9
ocaml(String) = 06ab5e6944c47322b9d305c0aa0b07ff
ocaml(CamlinternalLazy) = 227fb38c6dfc5c0f1b050ee46651eebe
ocaml(Evarutil) = 7ed9cd0756c03d2eaa170499ebcfe847
ocaml(Declarations) = 9b6e9960c4e7857ac9821c0bcc01856d
ocaml(Reductionops) = 87b9721f8f63b784fb93facef308b7de
ocaml(Tacexpr) = 53a4e6b6205e58eae44bc25b3dfc7850
ocaml(Pp_control) = 2db949c3c257a229f962ec5758c4cdf8
ocaml(Esubst) = 771af4025054928bb35d9ef08e52f4e3
ocaml(Classops) = 3e47eebf3cc8d1682019c33bc4e5378f
ocaml(Assumptions) = 30fbf8d78d8ed3d47ca16c8369444438
ocaml(Rtree) = 96b5d741b7db5ecc0067f79ce23e8195
ocaml(Mod_subst) = 944a18aa3b66049ab0ab119c273aeb7e
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
ocaml(Libobject) = 606bd8ad5949dfa65a16b6e768e59465
ocaml(Vernacexpr) = 1bd9b9b2917788443c78d4e98f203d85
ocaml(Conv_oracle) = c80baf87b36b314763ffae6a1b654bcb
ocaml(Nametab) = 4a8af666c69487590218d165f7c95a30
ocaml(Evar_refiner) = 6588904c8e5d573943bf561c3fe6b797
ocaml(Cases) = af6a82a6ca1d7aa5c2ad9514e22dc270
ocaml(Pervasives) = db723a1798b122e08919a2bfed062514
ocaml(Decl_expr) = dfda3d509f1f3b8d890bdd16cd23d466
ocaml(Genarg) = 9aa30ea43ac0035c189c6eb4beab0312
ocaml(Tactic_debug) = c955687056856ad081d52a48d8486aa7
ocaml(Coqlib) = 207dddc31e4d7c59ef2ae4dac78a650f
ocaml(Topconstr) = 6bff66a04ea5c30f50f4e539e55871ee
ocaml(Tactics) = 9b5ab5871badee298ad71c4a6fc7abfa
ocaml(Sign) = 53514d0cbc50f31c15143cc9580b8428
ocaml(Lazy) = aaa46201460de222b812caf2f6636244
ocaml(Goptions) = c09c6cc93205d063f2bdd18ac9cccd4b
ocaml(Sys) = 4fe60c54d4de0672924c1d4ee2053e46
ocaml(Egrammar) = 63d0f9bee0c43e4dde7299a8a05495a5
ocaml(Format) = e0de312c23ff9caec6c5bfa1f44a43b4
ocaml(Impargs) = fce1da9e8784e2fb47a1fd83ba5381d0
ocaml(Filename) = bc87b0a21cde095f477cca1f0abb32b8
ocaml(Grammar) = 62a81e78d8838c0f1b51aa279da1a82c
ocaml(Inductiveops) = aa4cf90b235001350e8c1747b7a5b861


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

 
ICM