summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/Elab.lean
diff options
context:
space:
mode:
authorSon Ho2024-04-11 19:40:08 +0200
committerSon Ho2024-04-11 19:40:08 +0200
commit86c3680b1f3f50b4c4e6198eebc145cadfff3876 (patch)
treec79ea2c4a35198d9011287db4767599b0c5c1c42 /backends/lean/Base/Diverge/Elab.lean
parent9c1773530a7056c161e69471b36eaa3603f6ed26 (diff)
parent4fb9c9f655a9ffc3b4a1a717988311c057c9c599 (diff)
Merge remote-tracking branch 'origin/main' into son/clean
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Diverge/Elab.lean1
1 files changed, 0 insertions, 1 deletions
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index d2dc3922..5db8ffed 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -1,7 +1,6 @@
import Lean
import Lean.Meta.Tactic.Simp
import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
import Base.Utils
import Base.Diverge.Base
import Base.Diverge.ElabBase