The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

Hi,

I have a module that defines several names, and I would like to make  
just a subset of them available as unqualified identifiers in some  
other scope.  From the documentation, I couldn't see a way to do this  
directly, but it seemed that defining an abbreviation for each one  
should be a reasonable workaround.

    Module Foo.
      Definition bar (x:nat) := x < 15.
    End Foo.
    Notation bar := Foo.bar.

However, this doesn't seem to work:

    Check (bar 4).
    (* This prints
              Foo.bar 4
                : Prop
       instead of:
              bar 4
                : Prop  *)

Is this a bug in the printing function?

Is there a better way to achieve the effect I'm after?

Thanks!

    - Benjamin