blob: 99183f2064f6a2c57ef16047256eff5b44846e34 (
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.
#[universes(template)] Inductive foo := f.
Show Match foo. (* no need to disambiguate *)
End A.
Module B.
#[universes(template)] Inductive foo := f.
(* local foo shadows A.foo, so constructor "f" needs disambiguation *)
Show Match A.foo.
End B.
|
