diff options
Diffstat (limited to 'test-suite/output/bug_10803.v')
| -rw-r--r-- | test-suite/output/bug_10803.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/bug_10803.v b/test-suite/output/bug_10803.v new file mode 100644 index 0000000000..1f2027d061 --- /dev/null +++ b/test-suite/output/bug_10803.v @@ -0,0 +1,14 @@ +Inductive Foo := foo. +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Bind Scope foo_scope with Foo. +Notation "'!'" := foo : foo_scope. +Definition of_foo {x : nat} {y : nat} (f : Foo) := f. +Notation a := (@of_foo O). +Notation b := (@a). +Check a !. +Check @a O !. +Check @b O. +Check @b O !. (* was failing *) +(* All are printed "a !", without making explicit the "0", which is + incidentally disputable *) |