Inlining of modules fails in some cases due to quirks in Coq's resolution of module names

[JasonGross]

Consider the files Foo.v:

Axiom A : Set.

and Bar.v:

Require Foo.Foo.

Module Export Top_DOT_Foo_DOT_Foo_DOT_Baz.
  Module Export Foo.
    Module Export Foo.
      Module Baz.
      End Baz.
    End Foo.
  End Foo.
End Top_DOT_Foo_DOT_Foo_DOT_Baz.

Import Foo.Foo.

Check A.

The command

coq_makefile Foo.v Bar.v -R . Foo | make -f - clean all

succeeds, because (I think) Coq refuses to mask absolute names and so the Import Foo.Foo refers to Foo.v, not to Top_DOT_Foo_DOT_Foo_DOT_Baz.Foo.Foo, even though the latter was declared later, which is how module resolution usually works.

This means that running

rm -f *.vo *.glob *.v.d; ~/coq-bug-finder/find-bug.py Bar.v out.v -R . Foo

gives

Error: The reference A was not found in the current environment.

rather than thinking that there is no error.

If the coq-devs see fit to implement feature request #4455, that could basically fix this. Otherwise, this will require careful thought.

[JasonGross]

Now that coq/coq#14537 is fixed, it may be possible to fix the issue with Import, at least, by adjusting all Import/Export statements while inlining the module.

[JasonGross]

I still wish the coqdevs would implement coq/coq#14541, which would admit a much cleaner solution to this problem.