aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4713.v
blob: 5d4d73be3f0fd568da2af878fe6e9b24f7bdc989 (plain)
1
2
3
4
5
6
7
8
9
10
Module Type T.
  Parameter t : Type.
End T.
Module M : T.
  Definition t := unit.
End M.

Fail Module Z : T with Module t := M := M.
Fail Module Z <: T with Module t := M := M.
Fail Declare Module Z : T with Module t := M.