From c3c0b8b8a208b05119edcedd5664a45ee3bf86d9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Mar 2022 05:26:33 -0700 Subject: [PATCH] chore: remove unnecessary code --- src/Lean/Elab/PreDefinition/Eqns.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index c6ff4c05b2..896ef5306e 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -287,8 +287,9 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do let rec go (mvarId : MVarId) : MetaM Unit := do if (← tryEqns mvarId) then return () - else if let some mvarId ← funext? mvarId then - go mvarId + -- Remark: we removed funext? from `mkEqnTypes` + -- else if let some mvarId ← funext? mvarId then + -- go mvarId else if let some mvarId ← simpMatch? mvarId then go mvarId else if let some mvarIds ← splitTarget? mvarId (splitIte := false) then