From eac410db4ee0e035c2de45c8d2f7e006bc6b1b1c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 14 Sep 2022 06:14:29 -0400
Subject: [PATCH] fix: fix tests

---
 tests/lean/1021.lean.expected.out | 8 ++++----
 tests/lean/run/core.lean          | 1 +
 tests/lean/run/depElim1.lean      | 1 +
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index ca069226ed..ef76cce863 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
-some { range := { pos := { line := 136, column := 41 },
+some { range := { pos := { line := 134, column := 41 },
     charUtf16 := 41,
-    endPos := { line := 142, column := 31 },
+    endPos := { line := 140, column := 31 },
     endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 136, column := 45 },
+  selectionRange := { pos := { line := 134, column := 45 },
     charUtf16 := 45,
-    endPos := { line := 136, column := 57 },
+    endPos := { line := 134, column := 57 },
     endCharUtf16 := 57 } }
diff --git a/tests/lean/run/core.lean b/tests/lean/run/core.lean
index 98f5250bf3..c8dd51954d 100644
--- a/tests/lean/run/core.lean
+++ b/tests/lean/run/core.lean
@@ -1,4 +1,5 @@
 import Lean.CoreM
+import Lean.MonadEnv
 
 open Lean
 open Lean.Core
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index e3c9978d01..d4b62db5a1 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -1,4 +1,5 @@
 import Lean.Meta.Match
+import Lean.Util.CollectLevelParams
 
 open Lean
 open Lean.Meta