chore: bump Std to leanprover-community/batteries#541

leanprover-community · Jan 18, 2024 · 1d98ebc · 1d98ebc
1 parent 2ae78a4
commit 1d98ebc
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/Aesop/Search/Expansion/Norm.lean b/Aesop/Search/Expansion/Norm.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Std.Data.Option.Basic
 import Aesop.RuleTac
 import Aesop.Search.Expansion.Basic
 import Aesop.Search.Expansion.Simp

diff --git a/Aesop/Util/EqualUpToIds.lean b/Aesop/Util/EqualUpToIds.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Lean.Elab.Tactic.Basic
 import Std.Lean.Meta.SavedState
 
 open Lean Lean.Meta

diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Lean.Meta.Tactic.Delta
 import Aesop.Util.Basic
 
 open Lean

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
  "type": "git",
  "subDir": null,
- "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
+ "rev": "1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36",
  "name": "std",
  "manifestFile": "lake-manifest.json",
  "inputRev": "main",