diff options
Diffstat (limited to 'test-suite/output/ShowMatch.v')
-rw-r--r-- | test-suite/output/ShowMatch.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v new file mode 100644 index 00000000..02b7eada --- /dev/null +++ b/test-suite/output/ShowMatch.v @@ -0,0 +1,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. |