Commit 2025-02-19 15:53 53c12145

fix: add missing withMainContext for hint (#22077) I’d love to add a test but I don’t know how to test what the suggestion widget shows. A simple test case is

example (P : Nat → Prop) : ∀ n, P n := by
  hint

which shows a _fvar on master.