feat: allow a general `evalTac` at `evalSepTactics`

[JovanGerb]

trafficstars

This PR generalizes evalSepTactics, so that users can use incremental elaboration in their own proof environment.

#lean4 > custom incremental elaboration

This was suggested by @mirefek

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7bd937580494311ecdb9502a7b5ab0ccf473bd44 --onto 1465c23e12f6f8b608ef944be4559b1b5e38f40a. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-27 19:02:53)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7bd937580494311ecdb9502a7b5ab0ccf473bd44 --onto 060b2fe46fe728934744ee52271b92ab74cbd5b4. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-29 13:19:18)

[JovanGerb]

changelog-language