From 923a7842b0abe8845530088918be102994cfc198 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 3 Nov 2024 01:04:21 -0500 Subject: [PATCH] chore: improve simp_alive_split (#771) --- SSA/Projects/InstCombine/TacticAuto.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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] + ) ) )