The Coq mailing list

[Marco Maggesi <maggesi AT math.unifi.it>]

Hi all,

I am trying to put Coq modules to work and there are something I find
annoying.  Very often I need to forget the structure of inductive type
of some elements like in the following example:

  Module Type Test_Sig.
  Variable X : Type.
  End Test_Sig.
  
  Module Test <: Test_Sig.
  Record X : Type := {
    x : Type
   }.
  End Test.

  Error: Signature components for label X do not match

The only solution I found is to change the definition of Test as
follows:

  Module Test <: Test_Sig.
  Record _X : Type := {
    x : Type
   }.
  Definition X : Type := _X.
  End Test.

Is it possible to do the same thing more directly?

Thanks,
marco