feat: allow turnstiles anywhere in location sequences

[jrr6]

This PR changes the syntax of location modifiers for tactics like simp and rw (e.g., simp at h ⊢) to allow the turnstile ⊢ to appear anywhere in the sequence of locations.

Closes #2278.

[nomeata]

Are you sure this PR doesn't work without stage0 update? Have you played with the preferNative flag, or the parseQuotWithCurrentStage?

[jrr6]

Are you sure this PR doesn't work without stage0 update? Have you played with the preferNative flag, or the parseQuotWithCurrentStage?

No matter what permutation of those two flags I use, if I don't do the intermediate stage0 update, I get the following error at a simp … at h ⊢ invocation in core:

Init/Data/String/Basic.lean:738:51: error: elaboration function for 'Lean.Parser.Tactic.locationTurnstile' has not been implemented
⊢

It seems as though the syntax change registers, but it's still using the built-in elaboration function from the old stage0, which is expecting the old syntax.