blob: 9cf6ad35b8f26bbaecb74f4e76fc8738dfeeb9a1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* 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.
End B.
|
