Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello, 

I wanted to try out Coq-8.5, but after building everything I noticed that I 
can apparently no longer import the basic ssreflect libraries without 
qualifying the name. I noticed that this appears to apply only to Ssreflect 
and  MathComp but not to the Coq standard libraries. Given that the MathComp 
theories have been patched to only use qualified imports, I assume this is 
not a problem with my local installation. Is this an intentional change or 
what is the issue here?

Btw. I noticed that loading ssreflect currently prints the license 
information twice:

chris@gentoo ~ $ coqtop
Welcome to Coq 8.5beta2 (June 2015)

Coq < Require ssreflect.
Toplevel input, characters 8-17:
> Require ssreflect.
>         ^^^^^^^^^
Error: Unable to locate library ssreflect.

Coq < Require Ssreflect.ssreflect.

Small Scale Reflection version 1.5 loaded.
Copyright 2005-2014 Microsoft Corporation and INRIA.
Distributed under the terms of the CeCILL-B license.

[Loading ML file ssreflect.cmxs ... done]

Small Scale Reflection version 1.5 loaded.
Copyright 2005-2014 Microsoft Corporation and INRIA.
Distributed under the terms of the CeCILL-B license.


-- 
Regards
Christian