From bf1e15181a2531a106fa643ca8e9233cb889af12 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Nov 2019 21:49:47 +0100
Subject: Fixes #4690: do not allow @f in notations when f is a notation
 variable.

---
 test-suite/bugs/bug_4690.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/bug_4690.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/bug_4690.v
new file mode 100644
index 0000000000..f50866a990
--- /dev/null
+++ b/test-suite/bugs/bug_4690.v
@@ -0,0 +1,3 @@
+(* Check that @f is not allowed in notation when f is a notation variable *)
+
+Fail Notation "# g" := (@g O) (at level 0).
-- 
cgit v1.2.3