coq-flocq-2.3.0-3.mga5.i586.rpm


Advertisement

Description

coq-flocq - Formalization of floating point numbers for Coq

Property Value
Distribution Mageia 5.1
Repository Mageia Core i586
Package name coq-flocq
Package version 2.3.0
Package release 3.mga5
Package architecture i586
Package type rpm
Installed size 5.09 MB
Download size 1.03 MB
Official Mirror distrib-coffee.ipsl.jussieu.fr
Flocq (Floats for Coq) is a floating-point formalization for the Coq
system.  It provides a comprehensive library of theorems on a
multi-radix multi-precision arithmetic.  It also supports efficient
numerical computations inside Coq.

Alternatives

Package Version Architecture Repository
coq-flocq-2.3.0-3.mga5.x86_64.rpm 2.3.0 x86_64 Mageia Core
coq-flocq - - -

Requires

Name Value
coq == 8.4pl4

Provides

Name Value
coq-flocq == 2.3.0-3.mga5
coq-flocq(x86-32) == 2.3.0-3.mga5

Download

Type URL
Binary Package coq-flocq-2.3.0-3.mga5.i586.rpm
Source Package coq-flocq-2.3.0-3.mga5.src.rpm

Install Howto

  1. Enable Mageia Core repository on Install and Remove Software
  2. Update packages list:
    # urpmi.update -a
  3. Install coq-flocq rpm package:
    # urpmi coq-flocq

Files

Path
/usr/lib/coq/user-contrib/Flocq/Flocq_version.v
/usr/lib/coq/user-contrib/Flocq/Flocq_version.vo
/usr/lib/coq/user-contrib/Flocq/Appli/Fappli_IEEE.v
/usr/lib/coq/user-contrib/Flocq/Appli/Fappli_IEEE.vo
/usr/lib/coq/user-contrib/Flocq/Appli/Fappli_IEEE_bits.v
/usr/lib/coq/user-contrib/Flocq/Appli/Fappli_IEEE_bits.vo
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_bracket.v
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_bracket.vo
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_digits.v
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_digits.vo
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_div.v
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_div.vo
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_ops.v
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_ops.vo
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_round.v
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_round.vo
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_sqrt.v
/usr/lib/coq/user-contrib/Flocq/Calc/Fcalc_sqrt.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FIX.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FIX.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FLT.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FLT.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FLX.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FLX.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FTZ.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_FTZ.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_Raux.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_Raux.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_Zaux.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_Zaux.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_defs.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_defs.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_digits.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_digits.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_float_prop.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_float_prop.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_generic_fmt.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_generic_fmt.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_rnd.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_rnd.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_rnd_ne.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_rnd_ne.vo
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_ulp.v
/usr/lib/coq/user-contrib/Flocq/Core/Fcore_ulp.vo
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_Sterbenz.v
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_Sterbenz.vo
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_div_sqrt_error.v
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_div_sqrt_error.vo
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_mult_error.v
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_mult_error.vo
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_plus_error.v
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_plus_error.vo
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_relative.v
/usr/lib/coq/user-contrib/Flocq/Prop/Fprop_relative.vo
/usr/share/doc/coq-flocq/AUTHORS
/usr/share/doc/coq-flocq/COPYING
/usr/share/doc/coq-flocq/NEWS
/usr/share/doc/coq-flocq/README
/usr/share/doc/coq-flocq/html/Flocq.Appli.Fappli_IEEE.html
/usr/share/doc/coq-flocq/html/Flocq.Appli.Fappli_IEEE_bits.html
/usr/share/doc/coq-flocq/html/Flocq.Calc.Fcalc_bracket.html
/usr/share/doc/coq-flocq/html/Flocq.Calc.Fcalc_digits.html
/usr/share/doc/coq-flocq/html/Flocq.Calc.Fcalc_div.html
/usr/share/doc/coq-flocq/html/Flocq.Calc.Fcalc_ops.html
/usr/share/doc/coq-flocq/html/Flocq.Calc.Fcalc_round.html
/usr/share/doc/coq-flocq/html/Flocq.Calc.Fcalc_sqrt.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_FIX.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_FLT.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_FLX.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_FTZ.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_Raux.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_Zaux.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_defs.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_digits.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_float_prop.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_generic_fmt.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_rnd.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_rnd_ne.html
/usr/share/doc/coq-flocq/html/Flocq.Core.Fcore_ulp.html
/usr/share/doc/coq-flocq/html/Flocq.Flocq_version.html
/usr/share/doc/coq-flocq/html/Flocq.Prop.Fprop_Sterbenz.html
/usr/share/doc/coq-flocq/html/Flocq.Prop.Fprop_div_sqrt_error.html
/usr/share/doc/coq-flocq/html/Flocq.Prop.Fprop_mult_error.html
/usr/share/doc/coq-flocq/html/Flocq.Prop.Fprop_plus_error.html
/usr/share/doc/coq-flocq/html/Flocq.Prop.Fprop_relative.html
/usr/share/doc/coq-flocq/html/coqdoc.css
/usr/share/doc/coq-flocq/html/index.html
/usr/share/doc/coq-flocq/html/toc.html

Changelog

2014-10-15 - umeabot <umeabot> 2.3.0-3.mga5
+ Revision: 740576
- Second Mageia 5 Mass Rebuild
2014-09-16 - umeabot <umeabot> 2.3.0-2.mga5
+ Revision: 678544
- Mageia 5 Mass Rebuild
2014-07-06 - pterjan <pterjan> 2.3.0-1.mga5
+ Revision: 644206
- 2.3.0
2013-11-29 - malo <malo> 2.1.0-1.mga4
+ Revision: 554097
- fix RPM group
- spec clean-up after import from Fedora
- imported package coq-flocq
2013-05-14 - Jerry James <loganjerry@gmail.com> - 2.1.0-5
- Rebuild for coq 8.4pl2
2013-02-13 - Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.1.0-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
2013-01-07 - Jerry James <loganjerry@gmail.com> - 2.1.0-3
- Rebuild for coq 8.4pl1
2012-08-21 - Jerry James <loganjerry@gmail.com> - 2.1.0-2
- Rebuild for coq 8.4
2012-07-28 - Jerry James <loganjerry@gmail.com> - 2.1.0-1
- New upstream release
- Build for OCaml 4.0.0 and coq 8.3pl4
2012-07-19 - Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.0.0-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild

See Also

Package Description
coq-ide-8.4pl4-5.mga5.i586.rpm The Coq Integrated Development Interface
corejava-format-1.22-5.mga5.noarch.rpm A class for formatting numbers that follows printf conventions
corejava-format-javadoc-1.22-5.mga5.noarch.rpm Javadoc for corejava-format
coreutils-8.23-6.mga5.i586.rpm The GNU core utilities: a set of tools commonly used in shell scripts
coreutils-doc-8.23-6.mga5.noarch.rpm Coreutils documentation in info format
corkscrew-2.0-14.mga5.i586.rpm Tool for tunneling SSH through HTTP proxies
coro-mock-1.0-7.mga5.noarch.rpm A mock library for compiling JVM coroutine-using code on JVMs without coroutines
coro-mock-javadoc-1.0-7.mga5.noarch.rpm Javadoc for coro-mock
corosync-2.3.4-4.mga5.i586.rpm The Corosync Cluster Engine and Application Programming Interfaces
corsixth-0.40-1.mga5.i586.rpm Open source clone of Theme Hospital
countdown-0.4.3-4.mga5.noarch.rpm Like sleep, only displays the amount of time remaining
countrycodes-1.0.5-12.mga5.i586.rpm Country code finder
courier-authdaemon-0.65.0-12.mga5.i586.rpm Courier authentication daemon
courier-authlib-0.65.0-12.mga5.i586.rpm Courier authentication library
courier-authlib-devel-0.65.0-12.mga5.i586.rpm Development libraries for the Courier authentication library
Advertisement
Advertisement