libssreflect-coq_1.3pl4-1_all.deb


Advertisement

Description

libssreflect-coq - small scale reflection library for Coq (theories)

Property Value
Distribution Debian 7 (Wheezy)
Repository Debian Main i386
Package name libssreflect-coq
Package version 1.3pl4
Package release 1
Package architecture all
Package type deb
Installed size 87.74 KB
Download size 15.34 MB
Official Mirror ftp.br.debian.org
The name Ssreflect stands for "small scale reflection", a style of
proof that evolved from the computer-checked proof of the Four Colour
Theorem and which leverages the higher-order nature of Coq's
underlying logic to provide effective automation for many small,
clerical proof steps. This is often accomplished by restating
("reflecting") problems in a more concrete form, hence the name. For
example, in the Ssreflect library, arithmetic comparison is not an
abstract predicate, but a function computing a boolean.
The Ssreflect distribution comprises two parts:
* A new tactic language, which promotes more structured, concise and
robust proof scripts, and is in fact independent from the "reflection"
proof style. It is implemented as a linkable extension to the Coq
system.
* A set of Coq libraries that provide core "reflection-oriented"
theories for basic combinatorics (roughly: arithmetic, lists, and
finite sets).
This package installs the full Ssreflect distribution.

Alternatives

Package Version Architecture Repository
libssreflect-coq_1.3pl4-1_all.deb 1.3pl4 all Debian Main
libssreflect-coq - - -

Requires

Name Value
coq-8.3pl4+3.12.1 -
libssreflect-ocaml >= 1.3pl4-1

Provides

Name Value
ssreflect -

Download

Type URL
Binary Package libssreflect-coq_1.3pl4-1_all.deb
Source Package ssreflect

Install Howto

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

Files

Path
/usr/bin/ssrcoq
/usr/lib/coq/user-contrib/Ssreflect/abelian.vo
/usr/lib/coq/user-contrib/Ssreflect/action.vo
/usr/lib/coq/user-contrib/Ssreflect/alt.vo
/usr/lib/coq/user-contrib/Ssreflect/automorphism.vo
/usr/lib/coq/user-contrib/Ssreflect/bigop.vo
/usr/lib/coq/user-contrib/Ssreflect/binomial.vo
/usr/lib/coq/user-contrib/Ssreflect/center.vo
/usr/lib/coq/user-contrib/Ssreflect/choice.vo
/usr/lib/coq/user-contrib/Ssreflect/commutator.vo
/usr/lib/coq/user-contrib/Ssreflect/cyclic.vo
/usr/lib/coq/user-contrib/Ssreflect/div.vo
/usr/lib/coq/user-contrib/Ssreflect/eqtype.vo
/usr/lib/coq/user-contrib/Ssreflect/extraspecial.vo
/usr/lib/coq/user-contrib/Ssreflect/extremal.vo
/usr/lib/coq/user-contrib/Ssreflect/finalg.vo
/usr/lib/coq/user-contrib/Ssreflect/finfun.vo
/usr/lib/coq/user-contrib/Ssreflect/fingraph.vo
/usr/lib/coq/user-contrib/Ssreflect/fingroup.vo
/usr/lib/coq/user-contrib/Ssreflect/finmodule.vo
/usr/lib/coq/user-contrib/Ssreflect/finset.vo
/usr/lib/coq/user-contrib/Ssreflect/fintype.vo
/usr/lib/coq/user-contrib/Ssreflect/frobenius.vo
/usr/lib/coq/user-contrib/Ssreflect/gfunctor.vo
/usr/lib/coq/user-contrib/Ssreflect/gproduct.vo
/usr/lib/coq/user-contrib/Ssreflect/gseries.vo
/usr/lib/coq/user-contrib/Ssreflect/hall.vo
/usr/lib/coq/user-contrib/Ssreflect/jordanholder.vo
/usr/lib/coq/user-contrib/Ssreflect/matrix.vo
/usr/lib/coq/user-contrib/Ssreflect/maximal.vo
/usr/lib/coq/user-contrib/Ssreflect/morphism.vo
/usr/lib/coq/user-contrib/Ssreflect/mxabelem.vo
/usr/lib/coq/user-contrib/Ssreflect/mxalgebra.vo
/usr/lib/coq/user-contrib/Ssreflect/mxpoly.vo
/usr/lib/coq/user-contrib/Ssreflect/mxrepresentation.vo
/usr/lib/coq/user-contrib/Ssreflect/nilpotent.vo
/usr/lib/coq/user-contrib/Ssreflect/path.vo
/usr/lib/coq/user-contrib/Ssreflect/perm.vo
/usr/lib/coq/user-contrib/Ssreflect/pgroup.vo
/usr/lib/coq/user-contrib/Ssreflect/poly.vo
/usr/lib/coq/user-contrib/Ssreflect/presentation.vo
/usr/lib/coq/user-contrib/Ssreflect/prime.vo
/usr/lib/coq/user-contrib/Ssreflect/primitive_action.vo
/usr/lib/coq/user-contrib/Ssreflect/quotient.vo
/usr/lib/coq/user-contrib/Ssreflect/seq.vo
/usr/lib/coq/user-contrib/Ssreflect/ssralg.vo
/usr/lib/coq/user-contrib/Ssreflect/ssrbool.vo
/usr/lib/coq/user-contrib/Ssreflect/ssreflect.vo
/usr/lib/coq/user-contrib/Ssreflect/ssrfun.vo
/usr/lib/coq/user-contrib/Ssreflect/ssrnat.vo
/usr/lib/coq/user-contrib/Ssreflect/sylow.vo
/usr/lib/coq/user-contrib/Ssreflect/tuple.vo
/usr/lib/coq/user-contrib/Ssreflect/vector.vo
/usr/lib/coq/user-contrib/Ssreflect/zmodp.vo
/usr/share/doc-base/ssreflect-library
/usr/share/doc/libssreflect-coq/ANNOUNCE.gz
/usr/share/doc/libssreflect-coq/README
/usr/share/doc/libssreflect-coq/README.Debian
/usr/share/doc/libssreflect-coq/changelog.Debian.gz
/usr/share/doc/libssreflect-coq/copyright
/usr/share/doc/libssreflect-coq/examples/changes13.v
/usr/share/doc/libssreflect-coq/examples/pg-ssr.el
/usr/share/doc/libssreflect-coq/examples/tutorial.v.gz
/usr/share/doc/libssreflect-coq/html/Ssreflect.abelian.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.action.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.alt.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.automorphism.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.bigop.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.binomial.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.center.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.choice.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.commutator.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.cyclic.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.div.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.eqtype.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.extraspecial.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.extremal.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.finalg.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.finfun.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.fingraph.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.fingroup.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.finmodule.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.finset.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.fintype.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.frobenius.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.gfunctor.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.gproduct.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.gseries.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.hall.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.jordanholder.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.matrix.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.maximal.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.morphism.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.mxabelem.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.mxalgebra.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.mxpoly.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.mxrepresentation.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.nilpotent.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.path.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.perm.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.pgroup.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.poly.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.presentation.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.prime.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.primitive_action.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.quotient.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.seq.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.ssralg.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.ssrbool.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.ssreflect.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.ssrfun.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.ssrnat.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.sylow.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.tuple.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.vector.html
/usr/share/doc/libssreflect-coq/html/Ssreflect.zmodp.html
/usr/share/doc/libssreflect-coq/html/coqdoc.css
/usr/share/doc/libssreflect-coq/html/index.html
/usr/share/doc/libssreflect-coq/html/toc.html
/usr/share/man/man1/ssrcoq.1.gz

Changelog

2012-06-09 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl4-1) unstable; urgency=low
* New upstream release
* Put debian/copyright in format 1.0
* Bump Standards-Version to 3.9.3
2012-04-01 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl2-4) unstable; urgency=medium
* Fix compilation with camlp5 6.05 and coq 8.3pl4
2012-03-06 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl2-3) unstable; urgency=low
* Recompile with camlp5 6.04 (no changes)
2011-12-25 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl2-2) unstable; urgency=low
* Rebuild with Coq 8.3pl3
- cherry-pick patch from coq-contrib to fix FTBFS with Coq 8.3pl3
2011-11-22 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl2-1) unstable; urgency=low
* New upstream release
2011-11-03 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl1-5) unstable; urgency=low
* Recompile with OCaml 3.12.1 (no changes)
* Bump Standards-Version to 3.9.2 (no changes)
2011-04-24 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl1-4) unstable; urgency=low
* Build theories only when explicitly asked (fixes FTBFS on armel as
a side-effect)
2011-04-21 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl1-3) unstable; urgency=low
* Upload to unstable
2011-03-31 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3pl1-1) experimental; urgency=low
* New upstream release
2011-03-15 - Stéphane Glondu <glondu@debian.org>
ssreflect (1.3-1) experimental; urgency=low
* New upstream release, compatible with Coq 8.3:
- remove 0001-Build-as-a-plugin.patch
- add 0001-Fix-tests-Make.patch
- this version is under CeCILL-B only; update debian/copyright
accordingly
* Bump Standards-Version to 3.9.1 (no changes)
* Update debian/watch

See Also

Package Description
libssreflect-ocaml-dev_1.3pl4-1_i386.deb small scale reflection extension for Coq (devt files)
libssreflect-ocaml_1.3pl4-1_i386.deb small scale reflection extension for Coq (plugin)
libsss-sudo-dev_1.8.4-2_i386.deb Communicator library for sudo -- development files
libsss-sudo0_1.8.4-2_i386.deb Communicator library for sudo
libst-dev_1.9-3_i386.deb State Threads Library - Development files
libst1_1.9-3_i386.deb State Threads Library
libstaden-read-dev_1.12.4-1_i386.deb development files for libstaden-read
libstaden-read1_1.12.4-1_i386.deb Staden library for reading and writing DNA sequencing results
libstapler-adjunct-codemirror-java_1.1-1_all.deb Codemirror JS library for use with stapler
libstapler-adjunct-timeline-java-doc_1.3+dfsg-1_all.deb Documentation for Stapler Timeline
libstapler-adjunct-timeline-java_1.3+dfsg-1_all.deb Timeline visualisation library for use with stapler
libstapler-java-doc_1.182-1_all.deb Documentation for libstapler-java
libstapler-java_1.182-1_all.deb Stapler HTTP request handling engine
libstarlink-ast-dev_7.0.4+dfsg-1_i386.deb Handle World Coordinate Systems in Astronomy (development package)
libstarlink-ast-doc_7.0.4+dfsg-1_all.deb Handle World Coordinate Systems in Astronomy (documentation)
Advertisement
Advertisement