chore: remove accidental grind trace options (#8311)

kim-em · web-flow · commit 29cc75531a5a · 2025-05-13T05:58:46.000Z
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
@@ -16,8 +16,6 @@ This file contains lemmas about `Std.DHashMap`. Most of the lemmas require
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 open Std.DHashMap.Internal
 
 set_option linter.missingDocs true
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -15,8 +15,6 @@ This file contains lemmas about `Std.Data.DHashMap.Raw`. Most of the lemmas requ
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 open Std.DHashMap.Internal
 
 set_option linter.missingDocs true
diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean
@@ -12,8 +12,6 @@ import Std.Data.ExtDHashMap.Basic
 This file contains lemmas about `Std.ExtDHashMap`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 
diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean
@@ -13,8 +13,6 @@ import Std.Data.ExtDHashMap.Lemmas
 This module contains lemmas about `Std.ExtHashMap`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 
diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean
@@ -13,8 +13,6 @@ import Std.Data.ExtHashSet.Basic
 This module contains lemmas about `Std.ExtHashSet`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
@@ -16,8 +16,6 @@ This module contains lemmas about `Std.Data.HashMap`. Most of the lemmas require
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
@@ -15,8 +15,6 @@ This module contains lemmas about `Std.Data.HashMap.Raw`. Most of the lemmas req
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
@@ -15,8 +15,6 @@ This module contains lemmas about `Std.Data.HashSet`. Most of the lemmas require
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
@@ -15,8 +15,6 @@ This module contains lemmas about `Std.Data.HashSet.Raw`. Most of the lemmas req
 is to provide an instance of `LawfulBEq α`.
 -/
 
-set_option trace.grind.ematch.pattern true
-
 set_option linter.missingDocs true
 set_option autoImplicit false
 
diff --git a/tests/lean/run/grind_map_uniform.lean b/tests/lean/run/grind_map_uniform.lean
