From bacba3d3ec0dd54d210bdf5045bc7e193c904b3c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Mar 2016 19:37:40 +0200
Subject: Adding a test for bug #1850.

---
 test-suite/bugs/closed/1850.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/1850.v

diff --git a/test-suite/bugs/closed/1850.v b/test-suite/bugs/closed/1850.v
new file mode 100644
index 0000000000..26b48093b7
--- /dev/null
+++ b/test-suite/bugs/closed/1850.v
@@ -0,0 +1,4 @@
+Parameter P : Type -> Type -> Type.
+Notation      "e |= t --> v" := (P e t v)     (at level 100, t at level 54).
+Fail Check (nat |= nat --> nat).
+
-- 
cgit v1.2.3