chore: remove workaround

2021-09-30 22:37:20 -07:00 · 2021-09-30 22:37:20 -07:00 · dba358067a
commit dba358067a
parent 3833363be8
1 changed files with 1 additions and 1 deletions
--- a/src/Lean/Meta/Tactic/Contradiction.lean
+++ b/src/Lean/Meta/Tactic/Contradiction.lean
@ -55,7 +55,7 @@ partial def elim (mvarId : MVarId) (fvarId : FVarId) : M Bool := do
              if (← elim subgoal.mvarId field.fvarId!) then
                return true
        return false
-      unless found == true do -- TODO: check why we need true here
+      unless found do
        return false
    return true