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 ++
 vernac/metasyntax.ml               | 3 +++
 2 files changed, 5 insertions(+)

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).
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 684036bc11..20a2a3218e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1233,6 +1233,9 @@ let find_precedence custom lev etyps symbols onlyprint =
             | _ ->
               user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
             end
+        | (ETPattern _ | ETBinder _), InConstrEntry when not onlyprint ->
+            (* Don't know exactly if we can make sense of this case *)
+            user_err Pp.(str "Binders or patterns not supported in leftmost position.")
         | (ETPattern _ | ETBinder _ | ETConstr _), _ ->
             (* Give a default ? *)
             if Option.is_empty lev then
-- 
cgit v1.2.3