diff options
| author | coqbot-app[bot] | 2020-09-28 16:18:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-28 16:18:52 +0000 |
| commit | 982c28216f3eb49abfd6b97c69b8fc116c813117 (patch) | |
| tree | 47edf047d93d4ead9d52afc795c812c34063a503 /test-suite | |
| parent | bd24f72a06343b375ad20aaa5b7296c2ad904a5c (diff) | |
| parent | a0090dc6930c1f0c60ca6144d1551019ecbcc837 (diff) | |
Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lonely notation at printing time.
Reviewed-by: ejgallego
Ack-by: maximedenes
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/bug_12908.out | 2 | ||||
| -rw-r--r-- | test-suite/output/bug_12908.v | 6 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out new file mode 100644 index 0000000000..fca6dde704 --- /dev/null +++ b/test-suite/output/bug_12908.out @@ -0,0 +1,2 @@ +forall m n : nat, m * n = (2 * m * n)%nat + : Prop diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v new file mode 100644 index 0000000000..558c9f9f6a --- /dev/null +++ b/test-suite/output/bug_12908.v @@ -0,0 +1,6 @@ +Definition mult' m n := 2 * m * n. +Module A. +(* Test hiding of a scoped notation by a lonely notation *) +Infix "*" := mult'. +Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. +End A. |