From a3c03857991f3f0d84edb109aaa68a03753699a6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 29 Apr 2019 09:50:26 +0000
Subject: Test-suite: add a case for issue #9180

---
 test-suite/output/bug_9180.out |  4 ++++
 test-suite/output/bug_9180.v   | 11 +++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 test-suite/output/bug_9180.out
 create mode 100644 test-suite/output/bug_9180.v

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.
-- 
cgit v1.2.3