diff options
| author | Hugo Herbelin | 2017-08-24 17:14:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-12 20:38:44 +0200 |
| commit | b9106a956c32e1352fcad5f0138a4e3ddee0474c (patch) | |
| tree | f45611447003783c5cc5dde40c3a0e268b08325d /test-suite | |
| parent | 86b9e40c2e2fd29c747a9f3ad20ebb2701210155 (diff) | |
Fixing bug #5693 (treating empty notation format as any format).
A trick in counting spaces in a format was making the empty notation
not behaving correctly.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 8 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 9d106d2dac..7bcd7b041c 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with | 1 => 1 end = p : forall x : nat, x = x -> Prop +bar 0 + : nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index b9985a594f..fe6c05c39e 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. |