chore: improve simp_alive_split (#771)

opencompl · Nov 3, 2024 · 923a784 · 923a784
1 parent cfae903
commit 923a784
Showing 1 changed file with 6 additions and 1 deletion.
diff --git 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]
+        )
       )
    )