Too much duplication with modules

[catalin-hritcu]

[Zoe might have discovered a nicer way?]

there is this Declare keyword, it might be helpful You can do something like that

Module Type M1.
 Parameter X : Type.
 Parameter x : X.
End M1.

Module Type M2.
 Parameter X : Type.
 Parameter y : X.
 Declare Module M3 : M1.
End M2.

https://coq.inria.fr/refman/Reference-Manual004.html paragraph 2.5.7