From 3bb14931395f6d77f634169e68ebcb3d8dd379ff Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 19 May 2026 03:53:44 -0700 Subject: [PATCH] refactor: remove use of `liftCommandElabM` from `Coinductive` (#13782) This PR eliminates the use of `liftCommandElabM` from the coinductive module. Context: `liftCommandElabM` was decided to be deprecated in issue #10674. --- src/Lean/Elab/Coinductive.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean index 311be55bbe..40431475be 100644 --- a/src/Lean/Elab/Coinductive.lean +++ b/src/Lean/Elab/Coinductive.lean @@ -411,10 +411,8 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do (value := originalCasesOn) (hints := .opaque) -- We apply the attribute so that the `cases` tactic can pick it up - liftCommandElabM - <| liftTermElabM - <| Term.applyAttributes - casesOnName #[{name := `cases_eliminator}, {name := `elab_as_elim}] + Term.TermElabM.run' <| Term.applyAttributes + casesOnName #[{name := `cases_eliminator}, {name := `elab_as_elim}] /-- Main entry point for elaborating mutual coinductive predicates. This function is called after