# ssreflect 1.5~rc1-2 source package in Ubuntu

## Changelog

ssreflect (1.5~rc1-2) unstable; urgency=low * Upload to unstable * Update Homepage -- Stéphane Glondu <email address hidden> Fri, 06 Dec 2013 08:28:06 +0100

## Upload details

- Uploaded by:
- Debian OCaml Maintainers on 2013-12-06

- Uploaded to:
- Sid

- Original maintainer:
- Debian OCaml Maintainers

- Architectures:
- any all

- Section:
- math

- Urgency:
- Low Urgency

## See full publishing history Publishing

Series | Published | Component | Section |
---|

## Downloads

File | Size | SHA-256 Checksum |
---|---|---|

ssreflect_1.5~rc1-2.dsc | 2.2 KiB | e163a9aec05463d705718e737241aee05ef320fc4105a39dbdf72fa77ee71baa |

ssreflect_1.5~rc1.orig.tar.gz | 199.2 KiB | f85d8ced769b6c38a499681a52480f2e0b9b7a0a8f028a3d35ecd1794ae64fc2 |

ssreflect_1.5~rc1-2.debian.tar.gz | 12.2 KiB | adac1360509c8424448b16890923a6e02c508772c322a710b26a0380f3b9f896 |

### Available diffs

- diff from 1.4-2 to 1.5~rc1-2 (799.1 KiB)

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

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.

- 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: small scale reflection extension for Coq (devt files)
This package is part of Ssreflect, the small scale reflection

extension for Coq. It provides the static native-code library, needed

to build custom toplevels, and the compiled interface.