File tree Expand file tree Collapse file tree 1 file changed +6
-6
lines changed Expand file tree Collapse file tree 1 file changed +6
-6
lines changed Original file line number Diff line number Diff line change @@ -122,7 +122,7 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState :
122122
123123structure DocString where
124124 content : String
125- range : Syntax.Range
125+ range : Elab. Syntax.Range
126126deriving ToJson
127127
128128/-- See `Lean.Elab.Modifiers` -/
@@ -139,7 +139,7 @@ deriving ToJson
139139structure DeclSignature where
140140 pp : String
141141 constants : Array Name
142- range : Syntax.Range
142+ range : Elab. Syntax.Range
143143deriving ToJson
144144
145145structure BinderView where
@@ -159,19 +159,19 @@ structure DeclBinders where
159159 pp : String
160160 groups : Array String
161161 map : Array BinderView
162- range : Syntax.Range
162+ range : Elab. Syntax.Range
163163deriving ToJson
164164
165165structure DeclType where
166166 pp : String
167167 constants : Array Name
168- range : Syntax.Range
168+ range : Elab. Syntax.Range
169169deriving ToJson
170170
171171structure DeclValue where
172172 pp : String
173173 constants : Array Name
174- range : Syntax.Range
174+ range : Elab. Syntax.Range
175175deriving ToJson
176176
177177local instance : ToJson OpenDecl where
@@ -194,7 +194,7 @@ deriving ToJson
194194
195195structure DeclarationInfo where
196196 pp: String
197- range : Syntax.Range
197+ range : Elab. Syntax.Range
198198 scope : ScopeInfo
199199 name : Name
200200 fullName : Name
You can’t perform that action at this time.
0 commit comments