From 56e247763f2aeeb947f706a0c19d5d6055000c60 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Jul 2021 15:22:51 -0700
Subject: [PATCH] fix: scope of the auto param at fields

---
 src/Lean/Elab/Structure.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 7da4074e12..34bbf19500 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -185,8 +185,11 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
           | some type =>
             let tac := binderTactic[2]
             let name ← Term.declareTacticSyntax tac
+            -- The tactic should be for binders+type.
+            -- It is safe to reset the binders to a "null" node since there is no value to be elaborated
+            let type ← `(forall $(binders.getArgs):bracketedBinder*, $type)
             let type ← `(autoParam $type $(mkIdentFrom tac name))
-            pure (binders, some type)
+            pure (mkNullNode, some type)
       else
         let (binders, type) := expandDeclSig fieldBinder[4]
         pure (binders, some type)