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 ()