chore: remove unused simp options

opencompl · Apr 7, 2024 · 15df4ae · 15df4ae
1 parent aa9d44e
commit 15df4ae
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/SSA/Core/Tactic.lean b/SSA/Core/Tactic.lean
@@ -57,7 +57,7 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident :
   `(tactic|
       (
       change_mlir_context $ll
-      simp (config := {failIfUnchanged := false, decide := false, unfoldPartialApp := true, zetaDelta := true}) only [
+      simp (config := {failIfUnchanged := false, decide := false }) only [
         Int.ofNat_eq_coe, Nat.cast_zero, DerivedCtxt.snoc, DerivedCtxt.ofCtxt,
         DerivedCtxt.ofCtxt_empty, Valuation.snoc_last,
         Com.denote, Expr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc,

diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
@@ -27,7 +27,7 @@ macro "simp_alive_peephole" : tactic =>
         dsimp only [Com.Refinement]
         intros Γv
         simp_peephole [InstCombine.Op.denote] at Γv
-        simp (config := {failIfUnchanged := false, unfoldPartialApp := true, zetaDelta := true}) only [
+        simp (config := {failIfUnchanged := false}) only [
             BitVec.Refinement, bind, Option.bind, pure,
             simp_llvm,
             BitVec.bitvec_minus_one