feat: injective theorem parameters should behave like regular ones

That is, they are eagerly activated

Author: leodemoura

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

@@ -117,7 +117,7 @@ def processParam (params : Grind.Params)
       throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
   | .inj =>
     let thm ← Grind.mkInjectiveTheorem declName
-    params := { params with inj := params.inj.insert thm }
+    params := { params with extraInj := params.extraInj.push thm }
   | .ext =>
     throwError "`[grind ext]` cannot be set using parameters"
   | .infer =>

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

@@ -35,6 +35,7 @@ structure Params where
   symPrios    : SymbolPriorities := {}
   casesTypes  : CasesTypes := {}
   extra       : PArray EMatchTheorem := {}
+  extraInj    : PArray InjectiveTheorem := {}
   norm        : Simp.Context
   normProcs   : Array Simprocs
   anchorRefs? : Option (Array AnchorRef) := none