From 34141026fa734a56e2a40c082cbf0f51f8e9a240 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 29 Jan 2025 15:31:29 +0000
Subject: [PATCH] chore: clean code

---
 src/Lean/Meta/Tactic/AC/Sharing.lean | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Meta/Tactic/AC/Sharing.lean b/src/Lean/Meta/Tactic/AC/Sharing.lean
index 8a0aa2405199..37d0240c8851 100644
--- a/src/Lean/Meta/Tactic/AC/Sharing.lean
+++ b/src/Lean/Meta/Tactic/AC/Sharing.lean
@@ -6,12 +6,12 @@ Authors: Alex Keizer
 prelude
 import Lean.Meta.Tactic.AC.Main
 import Init.Grind.Lemmas
-import Std.Tactic.BVDecide
+
+namespace Lean.Meta.AC.Sharing
 
 open Lean Meta
 
 /-! ### Types -/
-namespace AcNfBEq
 
 abbrev VarIndex := Nat
 
@@ -345,7 +345,6 @@ def post : Simp.Simproc := fun e => do
   | Eq ty lhs rhs =>
     canonicalizeEqWithSharing ty lhs rhs
   | BEq.beq ty inst lhs rhs =>
-    logInfo m!"@BEq.bEq {e}"
     canonicalizeBEqWithSharing ty inst lhs rhs
   | _ =>
     let mkApp2 op _ _ := e | return .continue
@@ -378,7 +377,6 @@ open Tactic
 
 def acNfHypMeta (goal : MVarId) (fvarId : FVarId) : MetaM (Option MVarId) := do
   goal.withContext do
-    throwError "yy"
     let simpCtx ← Simp.mkContext
       (simpTheorems  := {})
       (congrTheorems := (← getSimpCongrTheorems))
@@ -426,11 +424,9 @@ elab "ac_nf'" loc?:(location)? : tactic => do
       acNfTargetTactic'
       (← (← getMainGoal).getNondepPropHyps).forM acNfHypTactic'
 
-end AcNfBEq
 
 section Examples
 
-open AcNfBEq
 
 example {a b c d : Nat} : (a * b * (d + c)) == (b * a * (c + d)) := by
   ac_nf'