From 09dfd975936dd4db2ef4916637bd04507f1c74a7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Apr 2022 16:29:08 -0700 Subject: [PATCH] chore: remove temporary workaround --- src/Init/Data/AC.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean index faab678d29..6d332944d7 100644 --- a/src/Init/Data/AC.lean +++ b/src/Init/Data/AC.lean @@ -186,7 +186,7 @@ theorem Context.evalList_insert case inr => split case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] - case inr => simp_all [evalList, EvalInformation.evalOp]; simp [ih]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] -- TODO: remove `simp [ih]` after `update stage0` + case inr => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] theorem Context.evalList_sort_congr (ctx : Context α)