test-suite/bugs/closed/4713.v


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.