Library top.foo

Require Coq.Init.Logic.
Import Coq.Init.Logic.
Import Init.Logic.
Import Logic.
Require top.bar.
Import top.bar.
Module Export Foo.
  Module Export Bar.
    Module Export Baz.
      Axiom a : Type.
    End Baz.
  End Bar.
End Foo.
Import Foo.Bar.Baz.
Import Bar.Baz.
Import Baz.
Check Foo.Bar.Baz.a.
Check Bar.Baz.a.
Check Baz.a.
Check a.
Import top.bar.bar0.bar1.
Import bar.bar0.bar1.
Import bar0.bar1.
Import bar1.
Check top.bar.bar0.bar1.b.
Check bar.bar0.bar1.b.
Check bar0.bar1.b.
Check bar1.b.
Check b.