fix:

Author: leodemoura

src/Lean/Elab/Tactic/Grind/Param.lean

@@ -217,7 +217,10 @@ public def withParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic
   else
     let mut params := params
     if only then
-      params := { params with anchorRefs? := none }
+      params := { params with
+        ematch := {}
+        anchorRefs? := none
+      }
     params ← elabGrindParams params ps (only := only) (incremental := true)
     let anchorRefs? := params.anchorRefs?
     withReader (fun c => { c with params, ctx.anchorRefs? := anchorRefs? }) do

tests/lean/run/grind_indexmap_trace.lean

@@ -292,12 +292,18 @@ example (m : IndexMap α β) (a : α) (b : β) :
 example (m : IndexMap α β) (a : α) (b : β) :
     (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
   grind =>
-    instantiate only [insert, = mem_indices_of_mem, findIdx]
-    instantiate only [= getElem?_pos, = getElem?_neg]
+    instantiate only [findIdx, insert, = mem_indices_of_mem]
+    instantiate only [= getElem?_neg, = getElem?_pos]
     cases #1bba
-    next => instantiate only [findIdx]
-    next =>
-      instantiate only
-      instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
+    · instantiate only [findIdx]
+    · finish only [= HashMap.mem_insert, = HashMap.getElem_insert]
+
+example (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  grind =>
+    instantiate only [findIdx, insert, = mem_indices_of_mem]
+    instantiate only [= getElem?_neg, = getElem?_pos]
+    cases #1bba <;>
+      finish only [findIdx, = HashMap.mem_insert, = HashMap.getElem_insert]
 
 end IndexMap