Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Oct 10, 2012 at 11:06:15AM -0400, Andrej Bauer wrote:
> > I can't check because I'm on the move (again!) but the ssr library should 
> > no
> > longer depend on Bool, even if there is a leftover Require in the code. 
> > The
> > prelude file we really depend on is datatypes.v, mostly for 
> > interoperability
> > with other Coq developments. Some of the plugin functionality even depends
> > on it. But perhaps the HTT fork managed to retain that file?
> 
> As I said, we just ripped out the standard library because it would
> not compile and we are going to put back in whatever we can. I just
> look into the user contributions and there is a "ReleasedSsreflect"
> for 8.4. Is there something for the trunk?

Ignore "ReleasedSsreflect", it should not even exist!

I sent another mail with a pointer to the latest sources.

> P.S. ssreflect.ml4 is one of the scariest pieces of ocaml code I've
> seen, both in sheer length and form.

This is why I kind of offerend to look into it myself ;-)

Ciao
-- 
Enrico Tassi