bump to 4.7.0-rc2

lean-dojo · Mar 6, 2024 · 164914a · 164914a
1 parent bf7058b
commit 164914a
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/LeanCopilot/Frontend.lean b/LeanCopilot/Frontend.lean
@@ -2,7 +2,7 @@
    originally authored by Scott Morrison. -/
 import Lean
 import LeanCopilot.Options
-import Std.Tactic.TryThis
+import Lean.Meta.Tactic.TryThis
 import Std.Data.MLList.Basic
 import Std.Control.Nondet.Basic
 
@@ -12,7 +12,7 @@ open Lean Parser Elab Tactic
 set_option autoImplicit false
 
 
-open Std.Tactic.TryThis in
+open Lean.Meta.Tactic.TryThis in
 /--
 Construct a suggestion for a tactic.
 * Check the passed `MessageLog` for an info message beginning with "Try this: ".
@@ -56,7 +56,7 @@ def withoutInfoTrees (t : TacticM Unit) : TacticM Unit := do
   modifyInfoState fun s => { s with trees }
 
 
-open Std.Tactic.TryThis in
+open Lean.Meta.Tactic.TryThis in
 /--
 Run all tactics registered using `register_hint`.
 Print a "Try these:" suggestion for each of the successful tactics.

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": "f7e7cab885d8389b175ec90b08636d2c5f4dbb1f",
+   "rev": "28f42676168ea8431dbacf3e486ff25aabbf3322",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
+   "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.7.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.6.0
		leanprover/lean4:v4.7.0-rc2