Ssreflect Users Discussion List

[Bas Spitters <>]

@Andrej: I guess you are aware of VV  hLogic_r.v ?

https://groups.google.com/group/HomotopyTypeTheory/tree/browse_frm/month/2011-05/6a940826981cbf28?rnum=41&_done=/group/HomotopyTypeTheory/browse_frm/month/2011-05?&pli=1

On Wed, Oct 10, 2012 at 5:06 PM, 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?
>
> With kind regards,
>
> Andrej
>
> P.S. ssreflect.ml4 is one of the scariest pieces of ocaml code I've
> seen, both in sheer length and form.