The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

Does it work if you replace the `Require Import` with:

    Require Import
      Coq.Lists.List SetoidList implementations.list
      abstract_algebra interfaces.finite_sets interfaces.orders
      theory.lattices orders.lattices.

I mean, all the imports should be fully prefixed to avoid a maximum of 
ambiguities.

Best,
Guillaume

The 05/07/2015 19:46, Vadim Zaliva wrote:
> > On May 7, 2015, at 4:33 , Bas Spitters 
> > <b.a.w.spitters AT gmail.com
> > <mailto:b.a.w.spitters AT gmail.com>>
> >  wrote:
> >
> > I haven't thought deeply about case sensitivity, but if it requires a
> > minor change, I'd be willing to accept a pull request.
>
> Case-sensitivity problem is very annoying on MacOS. Here is a
> background: default MacOS file system is case-insensitive
> but case-preserving. So you you create file “A” it will be shown in
> upper case but you can open it either as “a” or “A”. Here is
> what happens with MathClasses:
>
> $ coqc -verbose -R . MathClasses -q implementations/list_finite_set.v
> Require Import
>    List SetoidList implementations.list
>    abstract_algebra interfaces.finite_sets interfaces.orders
>    theory.lattices orders.lattices.
> Warning: List.vo has been found in
> [ /Users/lord/tmp/math-classes/implementations ;
>    /Volumes/CoqLibs/coq/lib/coq/theories/Lists ];
> loading /Users/lord/tmp/math-classes/implementations/List.vo
> File "./implementations/list_finite_set.v", line 1, characters 0-148:
> Error: The file /Users/lord/tmp/math-classes/implementations/List.vo
> contains library
> MathClasses.implementations.list and not library
> MathClasses.implementations.List
>
> I think it is not really MathClasses problem. It could occur whenever
> you import some module of which you have several
> versions in your search path with names in different case.
>
> I think the proper solution is for coq to ignore files where file name
> does not match enclosed implementation, perhaps issuing a warning
> instead of an error. This should be a trivial patch to Coq itself. Maybe
> right now before 8.5 release it is a good way to put it in? MacOS users
> will benefit from it.
>
> Sincerely,
> Vadim Zaliva
>
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060
> Skype: vzaliva