feat: allow turnstiles anywhere in location sequences

leanprover · Feb 7, 2025 · 1533488 · 1533488
1 parent a690c20
commit 1533488
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 11 deletions.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -468,9 +468,7 @@ syntax locationTurnstile := patternIgnore(atomic("|" noWs "-") <|> "⊢")
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
--- Forthcoming definition after stage0 update:
--- syntax locationHyp := (ppSpace colGt (term:max <|> locationTurnstile))+
-syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
+syntax locationHyp := (ppSpace colGt (term:max <|> locationTurnstile))+
 
 /--
 Location specifications are used by many tactics that can operate on either the

diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
@@ -31,14 +31,10 @@ def expandLocation (stx : Syntax) : Location :=
   if arg.getKind == ``Parser.Tactic.locationWildcard then
     Location.wildcard
   else
-    -- Temporary workaround to accommodate stage0 update
-    if arg[1] matches .missing then
-      let locationHyps := arg[0].getArgs
-      let hypotheses := locationHyps.filter (·.getKind != ``Parser.Tactic.locationTurnstile)
-      let numTurnstiles := locationHyps.size - hypotheses.size
-      Location.targets hypotheses (numTurnstiles > 0)
-    else
-      Location.targets arg[0].getArgs (!arg[1].isNone)
+    let locationHyps := arg[0].getArgs
+    let hypotheses := locationHyps.filter (·.getKind != ``Parser.Tactic.locationTurnstile)
+    let numTurnstiles := locationHyps.size - hypotheses.size
+    Location.targets hypotheses (numTurnstiles > 0)
 
 def expandOptLocation (stx : Syntax) : Location :=
   if stx.isNone then