ssreflect 1.4-2 source package in Ubuntu
ssreflect (1.4-2) unstable; urgency=low * Bump debhelper compat level to 8 * Bump Standards-Version to 3.9.4 * Upload to unstable -- Stéphane Glondu <email address hidden> Thu, 09 May 2013 13:36:48 +0200
See full publishing history Publishing
No changes file available.
Binary packages built by this source
- libssreflect-coq: small scale reflection library for Coq (theories)
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
* A set of Coq libraries that provide core "reflection-
theories for basic combinatorics (roughly: arithmetic, lists, and
This package installs the full Ssreflect distribution.
- libssreflect-ocaml: small scale reflection extension for Coq (plugin)
This package is part of Ssreflect, the small scale reflection
extension for Coq. It provides 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.
- libssreflect-ocaml-dev: No summary available for libssreflect-ocaml-dev in ubuntu saucy.
No description available for libssreflect-
ocaml-dev in ubuntu saucy.