diff options
| author | Vincent Laporte | 2019-04-29 09:50:26 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-29 10:02:49 +0000 |
| commit | a3c03857991f3f0d84edb109aaa68a03753699a6 (patch) | |
| tree | 81b97d014a1a2d17d9e2cb1c935c0e5a4f984791 | |
| parent | 0e35f5f41b185309cbec3670ec8cfa8526e5fecf (diff) | |
Test-suite: add a case for issue #9180
| -rw-r--r-- | test-suite/output/bug_9180.out | 4 | ||||
| -rw-r--r-- | test-suite/output/bug_9180.v | 11 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out new file mode 100644 index 0000000000..ed4892b389 --- /dev/null +++ b/test-suite/output/bug_9180.out @@ -0,0 +1,4 @@ +Notation +"n .+1" := S n : nat_scope (default interpretation) +forall x : nat, x.+1 = x.+1 + : Prop diff --git a/test-suite/output/bug_9180.v b/test-suite/output/bug_9180.v new file mode 100644 index 0000000000..f221a94a50 --- /dev/null +++ b/test-suite/output/bug_9180.v @@ -0,0 +1,11 @@ +Notation succn := (Datatypes.S). + +Notation "n .+1" := (succn n) (at level 2, left associativity, + format "n .+1") : nat_scope. + +Locate ".+1". +(* Notation *) +(* "n .+1" := S n : nat_scope (default interpretation) *) +(** so Coq does not apply succn notation *) + +Check forall x : nat, x.+1 = x.+1. |