diff options
Diffstat (limited to 'test-suite/output/Notations.v')
| -rw-r--r-- | test-suite/output/Notations.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index b9985a594..fe6c05c39 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -291,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. Notation "1" := eq_refl. Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. +(* Check bug 5693 *) + +Module M. +Definition A := 0. +Definition bar (a b : nat) := plus a b. +Notation "" := A (format "", only printing). +Check (bar A 0). +End M. |