From a823ebdbe02ffa4a24e9768efabf49d502353bd8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Sep 2021 13:41:01 -0700
Subject: [PATCH] chore: make it clear how it is being parsed

We are planning to change the `<|>` precedence here.
---
 src/Init/Notation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index bf3e1bc542..0266342b14 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -324,7 +324,7 @@ syntax config := atomic("(" &"config") " := " term ")"
 syntax locationWildcard := "*"
 syntax locationHyp      := (colGt ident)+ ("⊢" <|> "|-")? -- TODO: delete
 syntax locationTargets  := (colGt ident)+ ("⊢" <|> "|-")?
-syntax location         := withPosition(" at " locationWildcard <|> locationHyp)
+syntax location         := withPosition(" at " (locationWildcard <|> locationHyp))
 
 syntax (name := change) "change " term (location)? : tactic
 syntax (name := changeWith) "change " term " with " term (location)? : tactic