libmathcomp-coq_1.5-3_all.deb


Advertisement

Description

libmathcomp-coq - Mathematical Components library for Coq (theories)

Distribution: Debian 8 (Jessie)
Repository: Debian Main amd64
Package name: libmathcomp-coq
Package version: 1.5
Package release: 3
Package architecture: all
Package type: deb
Installed size: 103.41 KB
Download size: 21.68 MB
Official Mirror: ftp.br.debian.org
The Mathematical Components library is an extensive library of formalized mathematics built using the Ssreflect extension for the Coq system.

Alternatives

    Download

    Source package: mathcomp

    Install Howto

    1. Update the package index:
      # sudo apt-get update
    2. Install libmathcomp-coq deb package:
      # sudo apt-get install libmathcomp-coq

    Files

    • /usr/lib/coq/user-contrib/MathComp/abelian.vo
    • /usr/lib/coq/user-contrib/MathComp/action.vo
    • /usr/lib/coq/user-contrib/MathComp/algC.vo
    • /usr/lib/coq/user-contrib/MathComp/algebraics_fundamentals.vo
    • /usr/lib/coq/user-contrib/MathComp/algnum.vo
    • /usr/lib/coq/user-contrib/MathComp/alt.vo
    • /usr/lib/coq/user-contrib/MathComp/automorphism.vo
    • /usr/lib/coq/user-contrib/MathComp/bigop.vo
    • /usr/lib/coq/user-contrib/MathComp/binomial.vo
    • /usr/lib/coq/user-contrib/MathComp/center.vo
    • /usr/lib/coq/user-contrib/MathComp/character.vo
    • /usr/lib/coq/user-contrib/MathComp/classfun.vo
    • /usr/lib/coq/user-contrib/MathComp/closed_field.vo
    • /usr/lib/coq/user-contrib/MathComp/commutator.vo
    • /usr/lib/coq/user-contrib/MathComp/countalg.vo
    • /usr/lib/coq/user-contrib/MathComp/cyclic.vo
    • /usr/lib/coq/user-contrib/MathComp/cyclotomic.vo
    • /usr/lib/coq/user-contrib/MathComp/div.vo
    • /usr/lib/coq/user-contrib/MathComp/extraspecial.vo
    • /usr/lib/coq/user-contrib/MathComp/extremal.vo
    • /usr/lib/coq/user-contrib/MathComp/falgebra.vo
    • /usr/lib/coq/user-contrib/MathComp/fieldext.vo
    • /usr/lib/coq/user-contrib/MathComp/finalg.vo
    • /usr/lib/coq/user-contrib/MathComp/finfun.vo
    • /usr/lib/coq/user-contrib/MathComp/fingraph.vo
    • /usr/lib/coq/user-contrib/MathComp/fingroup.vo
    • /usr/lib/coq/user-contrib/MathComp/finmodule.vo
    • /usr/lib/coq/user-contrib/MathComp/finset.vo
    • /usr/lib/coq/user-contrib/MathComp/frobenius.vo
    • /usr/lib/coq/user-contrib/MathComp/galois.vo
    • /usr/lib/coq/user-contrib/MathComp/generic_quotient.vo
    • /usr/lib/coq/user-contrib/MathComp/gfunctor.vo
    • /usr/lib/coq/user-contrib/MathComp/gproduct.vo
    • /usr/lib/coq/user-contrib/MathComp/gseries.vo
    • /usr/lib/coq/user-contrib/MathComp/hall.vo
    • /usr/lib/coq/user-contrib/MathComp/inertia.vo
    • /usr/lib/coq/user-contrib/MathComp/intdiv.vo
    • /usr/lib/coq/user-contrib/MathComp/integral_char.vo
    • /usr/lib/coq/user-contrib/MathComp/interval.vo
    • /usr/lib/coq/user-contrib/MathComp/jordanholder.vo
    • /usr/lib/coq/user-contrib/MathComp/matrix.vo
    • /usr/lib/coq/user-contrib/MathComp/maximal.vo
    • /usr/lib/coq/user-contrib/MathComp/morphism.vo
    • /usr/lib/coq/user-contrib/MathComp/mxabelem.vo
    • /usr/lib/coq/user-contrib/MathComp/mxalgebra.vo
    • /usr/lib/coq/user-contrib/MathComp/mxpoly.vo
    • /usr/lib/coq/user-contrib/MathComp/mxrepresentation.vo
    • /usr/lib/coq/user-contrib/MathComp/nilpotent.vo
    • /usr/lib/coq/user-contrib/MathComp/path.vo
    • /usr/lib/coq/user-contrib/MathComp/perm.vo
    • /usr/lib/coq/user-contrib/MathComp/pgroup.vo
    • /usr/lib/coq/user-contrib/MathComp/poly.vo
    • /usr/lib/coq/user-contrib/MathComp/polyXY.vo
    • /usr/lib/coq/user-contrib/MathComp/polydiv.vo
    • /usr/lib/coq/user-contrib/MathComp/presentation.vo
    • /usr/lib/coq/user-contrib/MathComp/prime.vo
    • /usr/lib/coq/user-contrib/MathComp/primitive_action.vo
    • /usr/lib/coq/user-contrib/MathComp/quotient.vo
    • /usr/lib/coq/user-contrib/MathComp/rat.vo
    • /usr/lib/coq/user-contrib/MathComp/ring_quotient.vo
    • /usr/lib/coq/user-contrib/MathComp/separable.vo
    • /usr/lib/coq/user-contrib/MathComp/ssralg.vo
    • /usr/lib/coq/user-contrib/MathComp/ssrint.vo
    • /usr/lib/coq/user-contrib/MathComp/ssrnum.vo
    • /usr/lib/coq/user-contrib/MathComp/sylow.vo
    • /usr/lib/coq/user-contrib/MathComp/tuple.vo
    • /usr/lib/coq/user-contrib/MathComp/vcharacter.vo
    • /usr/lib/coq/user-contrib/MathComp/vector.vo
    • /usr/lib/coq/user-contrib/MathComp/zmodp.vo
    • /usr/share/doc-base/mathcomp-library
    • /usr/share/doc/libmathcomp-coq/changelog.Debian.gz
    • /usr/share/doc/libmathcomp-coq/copyright
    • /usr/share/doc/libmathcomp-coq/html/MathComp.abelian.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.action.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.algC.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.algebraics_fundamentals.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.algnum.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.alt.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.automorphism.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.bigop.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.binomial.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.center.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.character.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.classfun.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.closed_field.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.commutator.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.countalg.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.cyclic.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.cyclotomic.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.div.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.extraspecial.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.extremal.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.falgebra.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.fieldext.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.finalg.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.finfun.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.fingraph.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.fingroup.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.finmodule.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.finset.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.frobenius.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.galois.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.generic_quotient.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.gfunctor.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.gproduct.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.gseries.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.hall.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.inertia.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.intdiv.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.integral_char.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.interval.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.jordanholder.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.matrix.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.maximal.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.morphism.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.mxabelem.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.mxalgebra.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.mxpoly.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.mxrepresentation.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.nilpotent.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.path.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.perm.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.pgroup.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.poly.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.polyXY.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.polydiv.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.presentation.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.prime.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.primitive_action.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.quotient.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.rat.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.ring_quotient.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.separable.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.ssralg.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.ssrint.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.ssrnum.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.sylow.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.tuple.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.vcharacter.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.vector.html
    • /usr/share/doc/libmathcomp-coq/html/MathComp.zmodp.html
    • /usr/share/doc/libmathcomp-coq/html/coqdoc.css
    • /usr/share/doc/libmathcomp-coq/html/index.html
    • /usr/share/doc/libmathcomp-coq/html/toc.html

    Changelog

    2014-08-04 - St├ęphane Glondu <glondu@debian.org> mathcomp (1.5-3) unstable; urgency=medium * Team upload * Recompile with coq 8.4pl4

    2014-03-19 - Enrico Tassi <gareuselesinge@debian.org> mathcomp (1.5-2) unstable; urgency=medium * Add dependency over libssreflect-coq (Closes: #742105)

    2014-03-11 - Enrico Tassi <gareuselesinge@debian.org> mathcomp (1.5-1) unstable; urgency=medium * Fix copyright file (I'm the packager, even if I've copied much from the ssreflect package Stephane made). * Initial package (Closes: #741345)

    Advertisement
    Advertisement