summaryrefslogtreecommitdiff
path: root/test-suite/output/Errors.v
blob: 75763f3b471d7bd778b1c3c659e59f6eb0a87177 (plain)
1
2
3
4
5
6
7
8
9
(* Test error messages *)

(* Test non-regression of bug fixed in r13486 (bad printer for module names) *)

Module Type S.
Parameter t:Type.
End S.
Module M : S.
Fail End M.