The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Hi,

I am trying to use the module system with Coq 8.1 and I don't seem to
get a sensible behavior. The following example defines an interface A (a
module type) and an implementation B (a module) for this interface. The
function g is an implementation detail (not in A, only in B) and it
should be hidden to the user of module B. So I am typing the following
script:

        Module Type A.
          Parameter T : Type.
          Parameter f : T -> T.
        End A.
        
        Module B : A.
          Definition T := nat.
          Definition g := S.
          Definition f := fun x : T => x.
        End B.
        
        Import B.
        Print T.
        Check (f 0).

Unfortunately, B can not be used at all, as Coq considers the type
definition T to be opaque. For the last two lines, Coq prints:

        *** [ T : Type ]
        Error: The term "0" has type "nat" while it is expected to have type 
"T"

The only way I have found so that I can use B is to replace the type
specification "B : A" with "B <: A". Coq now prints:

        T = nat
             : Set
        f 0
             : nat

Unfortunately, the implementation detail g now pollutes the global
scope. The documentation does not describe other ways of defining a
module of a given type. How can I get a usable module (T not opaque)
without leaking any implementations details (e.g. hundreds of
intermediate lemmas)?

Best regards,

Guillaume