aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2923.v
blob: 8a0003a3974a9cd2546d05d50de636238ee317cf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Module Type SIGNATURE1.
  Inductive IndType: Set :=
    | AConstructor.
End SIGNATURE1.

Module Type SIGNATURE2.
  Declare Module M1: SIGNATURE1.
End SIGNATURE2.

Module M2 (Module M1_: SIGNATURE1) : SIGNATURE2.
  Module M1 := M1_.
End M2.