# 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 | MD5 Checksum |
---|---|---|

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

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

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

### 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.