Ssreflect Users Discussion List

[Georges Gonthier <>]

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?
Cheers, Georges


Sent from my Windows Phone

---

From: Assia Mahboubi
Sent: 10/10/2012 15:43
To:
Subject: Re: Putting ssreflect on github

Hi Enrico and Andrej,

@Enrico : here it is : https://github.com/HoTT

see the INSTALL.txt instructions at the root of the directory since it is meant
to be compile with the forked coq.

From what I have seen this morning, one difficulty is that the HoTT library is
now to be compiled with a forked coq which has detached the standard Prelude
from the coq top level and also got rid of the std library.

@Andrej : for instance for now library Bool is no more accessible, is it? But in
order to benefit from the ssreflect tactics, you need to compile at least two
components : one is ssreflect.ml4, one is ssreflect.v (and a small ssrmatching.v
file as well). In their current state, the latter .v files depend on the
standard Bool library.

Best

assia

Le 10/10/2012 10:29, Enrico Tassi a écrit :
> On Wed, Oct 10, 2012 at 10:22:31AM -0400, Andrej Bauer wrote:
>> We are in coq trunk because we are making changes to the coq kernel.
>
> OK, could you give me a pointer? (I'm curious)
>
> Cheers
>