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

(limited to 'vernac/metasyntax.ml')

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