SEARCH
NEW RPMS
DIRECTORIES
ABOUT
FAQ
VARIOUS
BLOG

 
 

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

Name : gappalib-coq
Version : 0.17.0 Vendor : Fedora Project
Release : 1.fc16 Date : 2011-12-12 20:05:39
Group : Applications/Engineering Source RPM : gappalib-coq-0.17.0-1.fc16.src.rpm
Size : 1.42 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/16/x86_64

Content of RPM  Changelog  Provides Requires

Download
ftp.icm.edu.pl  gappalib-coq-0.17.0-1.fc16.x86_64.rpm
     

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

Requires :
ocaml(Option) = 0442e3e5203037a3eff12e730264ce9a
ocaml(Redexpr) = 38c4253305a6259c2839e023a19ec239
ocaml(Util) = 3fff17cfba1c46a9ee0500b731b2d418
ocaml(List) = 9c85fb419d52a8fd876c84784374e0cf
ocaml(Pptactic) = bb1ab81bf78ff88e1426c409562abcbe
ocaml(Notation) = eecb4e5de54e7837babd26f5a0c9d721
ocaml(Univ) = 2d2b9f5b7a2c0a2758eea57b59d54008
ocaml(Fstream) = 0638542c744443f2b176b95a5b211df9
ocaml(Extend) = 915c788d92f729998081e3e6e6e4ef0f
ocaml(Refiner) = 1b1c7e99281090f4e20946ec2f42d0da
ocaml(Retroknowledge) = 74ab3e6ad7ea1dee3580e62a32e88324
ocaml(Lexing) = 7d5623c54d065ad3f652261d2776959c
ocaml(Pcoq) = 36c2b343d679594c95d4a67b4618a32c
ocaml(Term) = 4ab47137eedd146fbdd7fa73157b2c9b
ocaml(Extrawit) = dc8fd6ed763fdcb281da1dc2dad0b02a
ocaml(Array) = 720848e0b508273805ef38d884a57618
ocaml(Cases) = 71be12dfab2a73e0fc29df93dfeede53
ocaml(Bigint) = a5fc4be04fd0ecb0f6ed15d8aafc4e1c
ocaml(Ppextend) = b8787e38cf274eb84babf5dcd4b48190
ocaml(Decl_kinds) = 96712336ea86ab2d6478174b7dbbd7aa
ocaml(Plexing) = af03d74fdd25c7f5adef6fedca18c3f1
ocaml(Compat) = d7503031e2d20b5f766ac706c395b783
ocaml(Constrintern) = 426638799c16e349e7ecec1d0bf723a7
ocaml(Stream) = cc2abcbdc5423e35862902ae0a0a4a7d
ocaml(Tacinterp) = d952002dbaa34342ec42e77f147969e5
flocq
ocaml(Evarutil) = 73430ad1d8fddb32969aa7dd23a833fd
ocaml(Pp) = 25f853c186a203ba8122b07ca95589d0
gappa
ocaml(Closure) = 1d59b1888740cbb7ae43679d85a0e065
rpmlib(FileDigests) <= 4.6.0-1
rpmlib(CompressedFileNames) <= 3.0.4-1
ocaml(Mod_subst) = d35838d18b6b4489abd3d107a297ac5e
ocaml(Map) = 971a915c5d6e79ba8c5a551e0767f582
ocaml(Token) = 1148e70ee439dfccb0930823a9dfa2ed
ocaml(Stdpp) = 4a9363c5c3c814dba55fb29c668cff31
ocaml(Libnames) = 940ebd6de65cc79d90d8d89d3a6ce3b6
ocaml(Set) = 7b178c9cf52b5cb8145441e1a0d309f5
ocaml(Hashtbl) = 9c86f7320512d6740a75017fd66156a8
ocaml(Dyn) = 57a60f030b39bf0e026afe272276ab77
ocaml(Tactic_debug) = c18075189033490da52f59a9973a0353
ocaml(Predicate) = 8b32cea1eab0d46cee1d01cc765ff771
ocaml(Environ) = a45caa1f11770cdcb1a4221ed6bb8ff6
ocaml(Flags) = 24caa56fb61169846604b56a994c62b1
ocaml(Tacmach) = 483a44cccf57b25e733d7afe2810618b
ocaml(Obj) = 3aeb33d11433c95bb62053c65665eb76
ocaml(Cerrors) = 34a3233d7c187061bc9914af788a4ece
ocaml(Tacticals) = 199fde59acbc836b2b1ffd034d28a94c
ocaml(Classops) = 369c3446b6291f7249eef8df30c8331a
ocaml(Clenv) = cb45b4b211ebaaf555a16d9b6401557f
ocaml(Evar_refiner) = 8dffd4f688199f3ad1adc81c19600305
ocaml(Scanf) = d7b5d0c4bd7ca9e180f113cbb292e7f2
ocaml(Proof_type) = c0340a3be06dbcf9d37b14435fe2327a
ocaml(Names) = a519db1ad3ac0dedf625bea9837003a4
ocaml(Proof_trees) = ee8d73894bd1bf40df829ce3f48e0a4a
ocaml(Cbytecodes) = c54b34663f061c25032c8f4f4c945863
ocaml(Lexer) = a57ea34559a7929e88ed326b2bfc65ee
ocaml(Buffer) = 40bf652f22a33a7cfa05ee1dd5e0d7e4
ocaml(Pattern) = a6ac6fa48a1ea8989c10dd688dfb5e42
ocaml(Tactics) = 8b28c29750b2339351ff9123c0b35fef
ocaml(Dumpglob) = f44d3636072a342edbfd849710b52969
ocaml(Evd) = 6fbac8732b8d9976a620218631f48a54
ocaml(Summary) = 8564a3500e9cd12c1132cf68df14d999
ocaml(runtime) = 3.12.0
ocaml(Rawterm) = 1b21fb46a9b92b9446773fc2f5dc7a15
ocaml(Lib) = 8ab5dc0b1ba10c13dd3fef3512953ce9
ocaml(Gramext) = 5dd2e0bee1e8f1d4eae3e3c00e14cf54
ocaml(Ploc) = 5379c25f9413f7df5d39ac3be287d946
rpmlib(PayloadIsXz) <= 5.2-1
ocaml(Pre_env) = a3022b845d28538bd52f334befd99e8b
ocaml(Int32) = c91c0bbb9f7670b10cdc0f2dcc57c5f9
ocaml(Unification) = 05e756b2a8ac2c6e9f39f79fe2410627
ocaml(String) = 06ab5e6944c47322b9d305c0aa0b07ff
ocaml(Cemitcodes) = b6fa9153a9a3dafa42c7cccf5ff66d02
coq(x86-64) = 8.3pl2
ocaml(CamlinternalLazy) = 227fb38c6dfc5c0f1b050ee46651eebe
ocaml(Reduction) = 3f47bae2fe1d5d8d80a01c5f5646b18a
ocaml(Declarations) = 9b6e9960c4e7857ac9821c0bcc01856d
ocaml(Pretyping) = 6ba609b96ea488fdf11476c2370239ae
ocaml(Tacexpr) = 53a4e6b6205e58eae44bc25b3dfc7850
ocaml(Pp_control) = 2db949c3c257a229f962ec5758c4cdf8
ocaml(Esubst) = 771af4025054928bb35d9ef08e52f4e3
ocaml(Rtree) = 96b5d741b7db5ecc0067f79ce23e8195
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
ocaml(Libobject) = 606bd8ad5949dfa65a16b6e768e59465
ocaml(Vernacexpr) = 1bd9b9b2917788443c78d4e98f203d85
ocaml(Conv_oracle) = c80baf87b36b314763ffae6a1b654bcb
ocaml(Termops) = 3053b4cfd4c7f75f7e860c4c4c7c2bc5
ocaml(Inductiveops) = 85c0b585fa825e8c410feb4660e6704b
ocaml(Nametab) = 4a8af666c69487590218d165f7c95a30
ocaml(Pervasives) = db723a1798b122e08919a2bfed062514
ocaml(Decl_expr) = dfda3d509f1f3b8d890bdd16cd23d466
ocaml(Genarg) = 9aa30ea43ac0035c189c6eb4beab0312
ocaml(Coqlib) = 207dddc31e4d7c59ef2ae4dac78a650f
ocaml(Impargs) = 4a34208d823fa6cb6b18805200211fd6
ocaml(Topconstr) = 6bff66a04ea5c30f50f4e539e55871ee
ocaml(Sign) = 53514d0cbc50f31c15143cc9580b8428
ocaml(Lazy) = aaa46201460de222b812caf2f6636244
ocaml(Reductionops) = fbc2136b02b392ec232d6dbf39ca9203
ocaml(Goptions) = c09c6cc93205d063f2bdd18ac9cccd4b
ocaml(Sys) = 4fe60c54d4de0672924c1d4ee2053e46
ocaml(Egrammar) = 63d0f9bee0c43e4dde7299a8a05495a5
ocaml(Coercion) = e4b61e5a95be6b10bd3af6746b0f51ec
ocaml(Format) = e0de312c23ff9caec6c5bfa1f44a43b4
ocaml(Filename) = bc87b0a21cde095f477cca1f0abb32b8
ocaml(Grammar) = 62a81e78d8838c0f1b51aa279da1a82c


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_proxy.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_user.vo
/usr/lib64/coq/user-contrib/Gappa/gappatac.cmo
/usr/lib64/coq/user-contrib/Gappa/gappatac.cmxs
/usr/share/doc/gappalib-coq-0.17.0
/usr/share/doc/gappalib-coq-0.17.0/AUTHORS
/usr/share/doc/gappalib-coq-0.17.0/COPYING
/usr/share/doc/gappalib-coq-0.17.0/NEWS
/usr/share/doc/gappalib-coq-0.17.0/README

 
ICM