Ssreflect Users Discussion List

[Assia Mahboubi <>]

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
>