fix

Author: kim-em

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

@@ -234,7 +234,7 @@ def elabGrindSimpTheorems (params : Grind.Params) : MetaM Grind.Params := do
           else
             .default false
         let thm ← Grind.mkEMatchTheoremForDecl declName kind symPrios
-        params := { params with ematch := params.ematch.insert thm }
+        params := { params with extra := params.extra.push thm }
       catch _ => pure () -- Silently skip theorems that fail
     | _ => pure () -- Skip non-declaration origins (fvars, etc.)
   return params

stage0/src/stdlib_flags.h

@@ -1,4 +1,5 @@
 #include "util/options.h"
+// Trigger update-stage0 for: add `simp` field to Init.Grind.Config
 
 namespace lean {
 options get_default_options() {