From bc173375ba8e76598e5fcc4b09a30575bf97f47c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Feb 2021 16:12:25 -0800 Subject: [PATCH] fix: missing `resolveGlobalConstNoOverload` --- src/Lean/Elab/Tactic/Induction.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 57db176492..39834a3f95 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -409,7 +409,7 @@ private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRe private def processResult (alts : Array Syntax) (result : Array Meta.InductionSubgoal) (numToIntro : Nat := 0) : TacticM Unit := do if alts.isEmpty then - setGoals $ result.toList.map fun s => s.mvarId + setGoals <| result.toList.map fun s => s.mvarId else unless alts.size == result.size do throwError! "mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({alts.size})" @@ -433,7 +433,7 @@ private def generalizeTerm (term : Expr) : TacticM Expr := do @[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focus do let targets ← stx[1].getSepArgs.mapM fun target => do - let target ← withMainMVarContext $ elabTerm target none + let target ← withMainMVarContext <| elabTerm target none generalizeTerm target let n ← generalizeVars stx targets if targets.size == 1 then @@ -446,7 +446,7 @@ private def generalizeTerm (term : Expr) : TacticM Expr := do if stx[2].isNone then throwError! "eliminator must be provided when multiple targets are used (use 'using ')" let elimId := stx[2][1] - let elimName := elimId.getId + let elimName ← withRef elimId do resolveGlobalConstNoOverload elimId.getId.eraseMacroScopes let elimInfo ← withRef elimId do getElimInfo elimName let (mvarId, _) ← getMainGoal let tag ← getMVarTag mvarId @@ -533,12 +533,12 @@ def evalCasesOn (target : Expr) (optInductionAlts : Syntax) : TacticM Unit := do processResult alts result def evalCasesUsing (elimId : Syntax) (targetRef : Syntax) (targets : Array Expr) (optInductionAlts : Syntax) : TacticM Unit := do - let elimName := elimId.getId + let elimName ← withRef elimId do resolveGlobalConstNoOverload elimId.getId.eraseMacroScopes let elimInfo ← withRef elimId do getElimInfo elimName let (mvarId, _) ← getMainGoal let tag ← getMVarTag mvarId withMVarContext mvarId do - let result ← withRef targetRef $ ElimApp.mkElimApp elimName elimInfo targets tag + let result ← withRef targetRef <| ElimApp.mkElimApp elimName elimInfo targets tag let elimArgs := result.elimApp.getAppArgs let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i] let motiveType ← inferType elimArgs[elimInfo.motivePos] @@ -547,7 +547,7 @@ def evalCasesUsing (elimId : Syntax) (targetRef : Syntax) (targets : Array Expr) withMVarContext mvarId do ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetsNew assignExprMVar mvarId result.elimApp - ElimApp.evalAlts elimInfo result.alts (getAltsOfOptInductionAlts optInductionAlts) (numEqs := targets.size) + ElimApp.evalAlts elimInfo result.alts (getAltsOfOptInductionAlts optInductionAlts) (numEqs := targets.size) (toClear := targetsNew) @[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focus do -- parser! nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts