exact? giving grind-y stuff

Stream: lean4

[Alex Meiburg]

On Lean v4.21.0-rc3, I just got the following output from exact?:

found a proof, but the corresponding tactic failed:
  (expose_names; exact fun a =>
    (fun {M} [Lean.Grind.IntModule M] {a b} => Lean.Grind.IntModule.sub_eq_zero_iff.mpr) (id (Eq.symm a)))

Besides the (slightly, but not very disappointing) fact that this failed, I think if exact? is starting to pull in very beta stuff from Lean.Grind that's a bad sign.

[Markus Himmel]

This is fixed by the stalled PR lean4#6672.

[Jovan Gerbscheid]

In my library search tactic, I filter using the name of the module where the lemma is defined (instead of the lemma name). So that means ignoring all constants from Init.Grind, Init.Omega and Mathlib.Tactic

[Kim Morrison]

Markus Himmel said:

This is fixed by the stalled PR lean4#6672.

Sorry about that. I've merged as is, if people want further changes in behaviour, please suggest them / make a PR!