From 48cef717aa677112bec3ad9ac72c09079fafa1b5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Aug 2020 16:35:00 -0700 Subject: [PATCH] feat: improve `tagUntaggedGoals` --- src/Lean/Elab/Tactic/Basic.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 50a7383148..b5ef8ea248 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -228,18 +228,20 @@ focusAux (do a ← tactic; done; pure a) /-- Use `parentTag` to tag untagged goals at `newGoals`. - If there are multiple new goals, they are named using `._` where `idx > 0`. - If there is only one new goal, then we just use `parentTag` -/ + If there are multiple new untagged goals, they are named using `._` where `idx > 0`. + If there is only one new untagged goal, then we just use `parentTag` -/ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do mctx ← getMCtx; -match newGoals with -| [g] => modifyMCtx $ fun mctx => if mctx.isAnonymousMVar g then mctx.renameMVar g parentTag else mctx -| _ => modifyMCtx $ fun mctx => +let numAnonymous := newGoals.foldl (fun n g => if mctx.isAnonymousMVar g then n + 1 else n) 0; +modifyMCtx fun mctx => let (mctx, _) := newGoals.foldl (fun (acc : MetavarContext × Nat) (g : MVarId) => let (mctx, idx) := acc; if mctx.isAnonymousMVar g then - (mctx.renameMVar g (parentTag ++ newSuffix.appendIndexAfter idx), idx+1) + if numAnonymous == 1 then + (mctx.renameMVar g parentTag, idx+1) + else + (mctx.renameMVar g (parentTag ++ newSuffix.appendIndexAfter idx), idx+1) else acc) (mctx, 1);