summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2603.v
blob: a556b9bf4067f47df131265ff6ffa8623e40b84f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Module Type T.
End T.

Declare Module K : T.

Module Type L.
Declare Module E : T.
End L.

Module M1 : L with Module E:=K.
Module E := K.
Fail Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
End M1.

Module M2 : L with Module E:=K.
Inductive t := E.
Fail Module E := K. (* Used to be accepted *)
Fail End M2. (* Used to be accepted *)