From fa6d35adfa080e3e419d420c6b522c1d4eb4f85a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Nov 2020 17:00:13 -0800
Subject: [PATCH] chore: fix tests

---
 tests/lean/run/instances.lean | 6 ++++--
 tests/lean/run/meta2.lean     | 2 +-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/tests/lean/run/instances.lean b/tests/lean/run/instances.lean
index 0c95b63c05..ce5c076d70 100644
--- a/tests/lean/run/instances.lean
+++ b/tests/lean/run/instances.lean
@@ -5,7 +5,9 @@ open Lean.Meta
 
 unsafe def tst1 : IO Unit :=
 withImportModules [{module := `Lean}] {} 0 fun env => do
-   let insts := env.getGlobalInstances;
-   IO.println (format insts)
+   let aux : MetaM Unit := do
+     let insts ← getGlobalInstancesIndex
+     IO.println (format insts)
+   discard <| aux.run |>.toIO {} { env := env }
 
 #eval tst1
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 2a7d21f890..7e3ed27e64 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -233,7 +233,7 @@ do print "----- tst14 -----";
    let stateM ← mkStateM nat;
    print stateM;
    let monad ← mkMonad stateM;
-   let globalInsts ← getGlobalInstances;
+   let globalInsts ← getGlobalInstancesIndex;
    let insts ← globalInsts.getUnify monad;
    print insts;
    pure ()