From a08ef5ffa2339db1993a52ec44402eea01e15665 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 16 Aug 2024 10:42:30 +0200
Subject: [PATCH] fix: remove partially copied code comment (#5070)

---
 src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 4b41029c9a..30216c4ec8 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -483,7 +483,6 @@ def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM Si
         if i + 1 = eqns.size then 0 else 1
       else
         100 - i
-      -- We assign very low priority to equational le
       d ← SimpTheorems.addConst d eqn (prio := prio)
     /-
     Even if a function has equation theorems,