test-suite/bugs/closed/bug_3974.v


1
2
3
4
5
6
7
8

Module Type S.
End S.

Module Type M (X : S).
  Fail Module P (X : S).
  (* Used to say: Anomaly: X already exists. Please report. *)
  (* Should rather say now: Error: X already exists. *)
End M.