summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3974.v
blob: b6be1595954bcad394bc8eb0fefb08fa95bf3e3b (plain)
1
2
3
4
5
6
7
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. *)