fix: make sure refine preserves pre-existing natural mvars

[thorimur]

Fixes #2434. refine currently fails to include pre-existing natural metavariables from the refined term in the resulting goal list. For example, constructor creates natural metavariables, and we can close the goals with refine alone:

example : True ∧ True := by -- (kernel) declaration has metavariables '_example'
  constructor
  · refine ?left
  · refine ?right

The source of this issue is a bug in withCollectingNewGoalsFrom in elabTermWithHoles when allowNaturalHoles is false. Metavariables are separated into natural and non-natural, and then any new unassigned natural mvars (as determined by their index) cause the tactic to be aborted. If the tactic isn't aborted here, the non-natural mvars are passed through to constitute the new goal list. However, this orphans any pre-existing "old" natural mvars.

This PR fixes this by changing the process of logging and aborting upon encountering new natural mvars into an unless allowedNaturalHoles do ...-style guard. If we pass that guard, then we don't need to filter the original list of mvars at all; it's guaranteed to be free of new natural mvars, as required.

[github-actions]

Thanks for your contribution! Please make sure to follow our Commit Convention.