Commit 2026-09-13 20:34 3fc1f443

feat(ClickSuggestions): support assigning metavariables in the goal (#43597) This PR lets #click_suggestions give suggestions that instantiate metavariables in the goal.

• The filtering heuristic is changed to accomodate dealing with metavariables better: Instead of filtering out all suggestions that introduce new metavariables, we allow new metavariables if they have been used to instantiate pre-existing metavariables.
• The apply and rw suggestions have support for filling in goals using local hypotheses. This is step is wrapped in withNewMCtxDepth to ensure it doesn't assign any metavariables.
• This PR also fixes the order in which apply goals are presented, by using the same reorderGoals that apply uses.
• Also some cleanup in ClickSuggestions.TryPremises, in order to have to pass around less arguments.