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

[Enrico Tassi <gareuselesinge@debian.org>]

On Thu, Dec 11, 2008 at 03:59:49PM +0100, Stephane Glondu wrote:
> 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

I'm interested in that software, but I'm a bit worried on how the
package could be done. Last time I used it, it was necessary to generate
a new coq toplevel... Is it now possible to load it on the fly?

Cheers
-- 
Enrico Tassi