The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

On May 3, 2007, at 5:03 AM, Guillaume Melquiond wrote:

>         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).

I believe that if you change the declaration of Module B to be

        Module B : A with Definition T := nat.

you will get the behavior that you are looking for.

(* **** *)
Coq < Print T.
T = nat
     : Type

Coq < Print g.
User error: g not a defined object

Coq < Check (f 0).
f 0
     : T
(* **** *)

There is a similar example in Section 2.5.7 of the reference manual.

Hope that helps,
Brian