From f48b822532872bb756bc04dfa453197ee6d35190 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 May 2022 14:06:42 -0700
Subject: [PATCH] feat: add field for storing `autoParam` information at
 `StructureFieldInfo`

We need this information when copying fields from parent structures.
We don't use hacks such as traversing the parent constructor type.
---
 src/Lean/Structure.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 3e5d6ea73f..3fff080c94 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -15,6 +15,7 @@ structure StructureFieldInfo where
   projFn     : Name
   subobject? : Option Name -- It is `some parentStructName` if it is a subobject, and `parentStructName` is the name of the parent structure
   binderInfo : BinderInfo
+  autoParam? : Option Expr := none
   deriving Inhabited, Repr
 
 def StructureFieldInfo.lt (i₁ i₂ : StructureFieldInfo) : Bool :=