blob: 02b7eada83a82cb5f56ca6c771d8c703f9639b2a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Bug 5546 complained about unqualified constructors in Show Match output,
when qualification is needed to disambiguate them
*)
Module A.
Inductive foo := f.
Show Match foo. (* no need to disambiguate *)
End A.
Module B.
Inductive foo := f.
(* local foo shadows A.foo, so constructor "f" needs disambiguation *)
Show Match A.foo.
|
