diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean index a9b80255d..aa1ffb054 100644 --- a/SSA/Projects/InstCombine/TacticAuto.lean +++ b/SSA/Projects/InstCombine/TacticAuto.lean @@ -228,7 +228,12 @@ macro "bv_compare'": tactic => macro "simp_alive_split": tactic => `(tactic| ( - repeat(all_goals split; all_goals simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl]) + all_goals try intros + repeat( + all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl] + any_goals split + all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl] + ) ) )