Ssreflect Users Discussion List

[Guillaume Melquiond <>]

On 26/06/2015 10:52, Christian Doczkal wrote:
> 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?

This is an intentional change that applies to all the user libraries 
(not just Ssreflect). Basically, the Coq developers started to worry 
about the conflicts between similarly-named files across several user 
libraries, so they enforced full-qualification for users of libraries.

As you discovered, you can simply add "Ssreflect." before all your 
imports. If you don't want to do it by hand, you can also use the 
update-require script shipped with Coq 8.5 to convert a whole development.

If you don't care about backward-compatibility, you can also use the 
"From Ssreflect Require" syntax provided in Coq 8.5.

Best regards,

Guillaume