Skip to content

Commit d0d8709

Browse files
committed
chore: remove workaround
1 parent 3f7a73e commit d0d8709

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/Lean/Meta/Tactic/Grind/SearchM.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,6 @@ Returns `some gen` if a new goal was found for a choice point with generation `g
169169
and returns `none` otherwise.
170170
-/
171171
def nextGoal? : SearchM (Option Nat) := do
172-
if true then nextChronoGoal? else -- TODO: FIX
173172
let mut choices := (← get).choiceStack
174173
if choices.isEmpty then
175174
return none -- done

0 commit comments

Comments
 (0)