From df665eb8fc58fa2e61f669b3004c96f2d89f9407 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Nov 2020 08:28:01 -0800
Subject: [PATCH] fix: notation

---
 src/Init/NotationExtra.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 4e41424674..a5ee409bca 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -69,7 +69,7 @@ private def mkHintBody (cs : Array Syntax) (p : Syntax) : MacroM Syntax := do
   return body
 
 macro_rules
-  | `(unif_hint $bs* where $cs* |- $p) => do
+  | `(unif_hint $bs:explicitBinder* where $cs* |- $p) => do
     let body ← mkHintBody cs p
     `(@[unificationHint] def hint $bs:explicitBinder* : Sort _ := $body)
   | `(unif_hint $n:ident $bs* where $cs* |- $p) => do