From c159432fcbc92fb17892d4a5268d68111b3e2d24 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Nov 2019 16:09:11 -0800
Subject: [PATCH] chore: use new tracing kind

---
 library/Init/Lean/Meta/LevelDefEq.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/Init/Lean/Meta/LevelDefEq.lean b/library/Init/Lean/Meta/LevelDefEq.lean
index 3844ca5def..59e1aa4fb8 100644
--- a/library/Init/Lean/Meta/LevelDefEq.lean
+++ b/library/Init/Lean/Meta/LevelDefEq.lean
@@ -58,7 +58,7 @@ partial def isLevelDefEqAux : Level → Level → MetaM Bool
   if lhs == rhs then
     pure true
   else do
-    trace! `type_context.level_is_def_eq (lhs ++ " =?= " ++ rhs);
+    trace! `Meta.isLevelDefEq.step (lhs ++ " =?= " ++ rhs);
     lhs' ← instantiateLevelMVars lhs;
     let lhs' := lhs'.normalize;
     rhs' ← instantiateLevelMVars rhs;