The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Dear all,

I am not sure if this list is the better place to ask questions about tactic 
implementation in Ocaml, but I would like to learn how one can have access to 
the fields of Coq's parameterized modules, and to module types.

For instance, suppose we have the following Coq code:

<<<
Module Type mt.
        
        Parameter t : Type.

End mt.

Module MT(m:mt).
        
        Import m.

        Inductive mt_ind : Type :=
        |mt0 : m.t -> mt_ind.
        
End MT.
>>>

In this case, how can I have access to [t] in the case of the module type 
[mt], and to the inductive type [mt_ind] ? 

Best regards,
        David Pereira.