Bug#508468: ITP: ssreflect -- small scale reflection extension for the Coq proof assistant

[Stephane Glondu <steph@glondu.net>]

Package: wnpp
Severity: wishlist
Owner: Stephane Glondu <steph@glondu.net>

* Package name    : ssreflect
  Version         : 1.1
  Upstream Author : Georges Gonthier (Microsoft Research - Inria Joint Centre)
* URL             : http://www.msr-inria.inria.fr/Projects/math-components
* License         : CeCILL-B
  Programming Lang: OCaml, Coq
  Description     : small scale reflection extension library for the Coq proof assistant

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

-- System Information:
Debian Release: lenny/sid
  APT prefers testing
  APT policy: (990, 'testing'), (500, 'unstable'), (1, 'experimental')
Architecture: i386 (i686)