Skip to content

Commit 074516d

Browse files
committed
Revert "merge only parentDecl range"
This reverts commit 83b011c.
1 parent 83b011c commit 074516d

File tree

1 file changed

+2
-13
lines changed

1 file changed

+2
-13
lines changed

src/Lean/Elab/InfoTree/Main.lean

Lines changed: 2 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -51,19 +51,8 @@ def PartialContextInfo.mergeIntoOuter?
5151
panic! "Unexpected incomplete InfoTree context info."
5252
| .autoImplicitCtx _, none =>
5353
panic! "Unexpected incomplete InfoTree context info."
54-
| .commandCtx innerInfo, some outer => Id.run do
55-
-- There is no reasonable way to merge the two environments in general, so we only do it for
56-
-- relevant extensions:
57-
-- * `declRangeExt` is queried by e.g. the call hierarchy handler to get the range of the
58-
-- current declaration, but that one is set only at the very end of the `def` elaborator, so
59-
-- we must merge it into inner environments saved when e.g. finishing elaboration of the body.
60-
let mut env := innerInfo.env
61-
if let some parentDecl := outer.parentDecl? then
62-
env := declRangeExt.modifyState (asyncMode := .local) env fun s =>
63-
match declRangeExt.getState (asyncMode := .local) outer.env |>.find? parentDecl with
64-
| some range => s.insert parentDecl range
65-
| none => s
66-
some { outer with toCommandContextInfo := { innerInfo with env } }
54+
| .commandCtx innerInfo, some outer =>
55+
some { outer with toCommandContextInfo := innerInfo }
6756
| .parentDeclCtx innerParentDecl, some outer =>
6857
some { outer with parentDecl? := innerParentDecl }
6958
| .autoImplicitCtx innerAutoImplicits, some outer =>

0 commit comments

Comments
 (0)