doc:

Author: leodemoura

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

@@ -130,6 +130,7 @@ def mkGrindParams
   trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
   return params
 
+-- **TODO**: Remove `Grind.Trace`
 def grind
     (mvarId : MVarId) (config : Grind.Config)
     (only : Bool)

src/Lean/Elab/Tactic/Try.lean

@@ -378,6 +378,7 @@ where
                     $tacs2*)
       modify (·.push tac)
 
+-- **TODO**: Use `finish?` infrastructure
 private def evalSuggestGrindTrace : TryTactic := fun tac => do
   match tac with
   | `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?) =>