From 26a456cbf1e8abc5c033090b59892b314d7e7142 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 Sep 2020 21:41:48 +0200
Subject: Fixing printing part of #13078 (anomaly with binding notations in
 patterns).

We prevent notations involving binders (i.e. names or patterns) to be
used for printing in "match" patterns. The computation is done in
"has_no_binders_type", controlling uninterpretation.
---
 test-suite/bugs/closed/bug_13078.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13078.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13078.v b/test-suite/bugs/closed/bug_13078.v
new file mode 100644
index 0000000000..1bd32d0576
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13078.v
@@ -0,0 +1,8 @@
+(* Check that rules with patterns are not registered for cases patterns *)
+Module PrintingTest.
+Declare Custom Entry test.
+Notation "& x" := (Some x) (in custom test at level 0, x pattern).
+Check fun x => match x with | None => None | Some tt => Some tt end.
+Notation "& x" := (Some x) (at level 0, x pattern).
+Check fun x => match x with | None => None | Some tt => Some tt end.
+End PrintingTest.
-- 
cgit v1.2.3


From 116e82b44946998dad06b33b3fdc2516fca42fcc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 26 Sep 2020 14:13:09 +0200
Subject: Addressing parsing part #13078.

We don't give sense to pattern/binders in leftmost position.
---
 test-suite/bugs/closed/bug_13078.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13078.v b/test-suite/bugs/closed/bug_13078.v
index 1bd32d0576..ec04408fd1 100644
--- a/test-suite/bugs/closed/bug_13078.v
+++ b/test-suite/bugs/closed/bug_13078.v
@@ -6,3 +6,5 @@ Check fun x => match x with | None => None | Some tt => Some tt end.
 Notation "& x" := (Some x) (at level 0, x pattern).
 Check fun x => match x with | None => None | Some tt => Some tt end.
 End PrintingTest.
+
+Fail Notation "x &" := (Some x) (at level 0, x pattern).
-- 
cgit v1.2.3