chore: remove leftover traces

leanprover · Apr 24, 2024 · 70a0ce4 · 70a0ce4
1 parent 28f0c03
commit 70a0ce4
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
@@ -133,7 +133,6 @@ private def mkInjectiveTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
     | return ()
   let value ← mkInjectiveTheoremValue ctorVal.name type
   let name := mkInjectiveTheoremNameFor ctorVal.name
-  trace[Meta.injective] "theorem {name} : {type} := {value}"
   addDecl <| Declaration.thmDecl {
     name
     levelParams := ctorVal.levelParams
@@ -165,7 +164,6 @@ private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
     | return ()
   let value ← mkInjectiveEqTheoremValue ctorVal.name type
   let name := mkInjectiveEqTheoremNameFor ctorVal.name
-  trace[Meta.injective] "theorem {name} : {type} := {value}"
   addDecl <| Declaration.thmDecl {
     name
     levelParams := ctorVal.levelParams