From 80cf782bc6f61c6fcc7d0251b2b42bf44857289b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 10 Feb 2025 21:56:20 +1100
Subject: [PATCH] chore: rename simp sets (#7018)

This is preliminary to #7017; we'll need an update-stage0 before the
actual rename can take place.
---
 src/Lean/Elab/Tactic/BoolToPropSimps.lean | 5 +++++
 src/Lean/Elab/Tactic/Omega/Frontend.lean  | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/src/Lean/Elab/Tactic/BoolToPropSimps.lean b/src/Lean/Elab/Tactic/BoolToPropSimps.lean
index 681680461c..e14ce2fc3d 100644
--- a/src/Lean/Elab/Tactic/BoolToPropSimps.lean
+++ b/src/Lean/Elab/Tactic/BoolToPropSimps.lean
@@ -7,6 +7,11 @@ Authors: Tobias Grosser
 prelude
 import Lean.Meta.Tactic.Simp.Attr
 
+builtin_initialize bool_to_prop : Lean.Meta.SimpExtension ←
+  Lean.Meta.registerSimpAttr `bool_to_prop
+    "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
+
+@[deprecated bool_to_prop (since := "2025-02-10")]
 builtin_initialize boolToPropSimps : Lean.Meta.SimpExtension ←
   Lean.Meta.registerSimpAttr `boolToPropSimps
     "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index e985a8b9ad..ce08b338ab 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -689,6 +689,11 @@ def evalOmega : Tactic
     omegaTactic cfg
   | _ => throwUnsupportedSyntax
 
+builtin_initialize bitvec_to_nat : SimpExtension ←
+  registerSimpAttr `bitvec_to_nat
+    "simp lemmas converting `BitVec` goals to `Nat` goals"
+
+@[deprecated bitvec_to_nat (since := "2025-02-10")]
 builtin_initialize bvOmegaSimpExtension : SimpExtension ←
   registerSimpAttr `bv_toNat
     "simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"