chore: adaptations for leanprover/lean4#3123

leanprover-community · Jan 4, 2024 · 1200cde · 1200cde
1 parent d8610e1
commit 1200cde
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/Std/Lean/Meta/DiscrTree.lean b/Std/Lean/Meta/DiscrTree.lean
@@ -165,11 +165,11 @@ Inserts a new key into a discrimination tree,
 but only if it is not of the form `#[*]` or `#[=, *, *, *]`.
 -/
 def insertIfSpecific [BEq α] (d : DiscrTree α)
-    (keys : Array DiscrTree.Key) (v : α) (config : WhnfCoreConfig) : DiscrTree α :=
+    (keys : Array DiscrTree.Key) (v : α) : DiscrTree α :=
   if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
     d
   else
-    d.insertCore keys v config
+    d.insertCore keys v
 
 variable {m : Type → Type} [Monad m]
 

diff --git a/Std/Tactic/Ext/Attr.lean b/Std/Tactic/Ext/Attr.lean
@@ -39,7 +39,7 @@ initialize extExtension :
     SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
   registerSimpleScopedEnvExtension {
     addEntry := fun { tree, erased } thm =>
-      { tree := tree.insertCore thm.keys thm extExt.config, erased := erased.erase thm.declName }
+      { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName }
     initial := {}
   }
 

diff --git a/Std/Tactic/Relation/Rfl.lean b/Std/Tactic/Relation/Rfl.lean
@@ -24,7 +24,7 @@ def reflExt.config : WhnfCoreConfig := {}
 initialize reflExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
   registerSimpleScopedEnvExtension {
-    addEntry := fun dt (n, ks) => dt.insertCore ks n reflExt.config
+    addEntry := fun dt (n, ks) => dt.insertCore ks n
     initial := {}
   }
 

diff --git a/Std/Tactic/Relation/Symm.lean b/Std/Tactic/Relation/Symm.lean
@@ -25,7 +25,7 @@ def symmExt.config : WhnfCoreConfig := {}
 initialize symmExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
   registerSimpleScopedEnvExtension {
-    addEntry := fun dt (n, ks) => dt.insertCore ks n symmExt.config
+    addEntry := fun dt (n, ks) => dt.insertCore ks n
     initial := {}
   }
 

diff --git a/Std/Util/Cache.lean b/Std/Util/Cache.lean
@@ -146,7 +146,7 @@ def DiscrTreeCache.mk [BEq α] (profilingName : String)
     IO (DiscrTreeCache α) :=
   let updateTree := fun name constInfo tree => do
     return (← processDecl name constInfo).foldl (init := tree) fun t (k, v) =>
-      t.insertCore k v config
+      t.insertCore k v
   let addDecl := fun name constInfo (tree₁, tree₂) =>
     return (← updateTree name constInfo tree₁, tree₂)
   let addLibraryDecl := fun name constInfo (tree₁, tree₂) =>