From 40f99327e9be9e6e00daac0950292ff044d1ae7d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Oct 2020 11:35:54 -0700 Subject: [PATCH] fix: missing `withMainMVarContext` --- src/Lean/Elab/Tactic/Induction.lean | 2 +- tests/lean/run/inductionTacticBug.lean | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/inductionTacticBug.lean diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 009edab774..f9698936d0 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -195,7 +195,7 @@ private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAl withAlts : Parser := optional (" with " >> inductionAlts) usingRec : Parser := optional (" using " >> ident) ``` -/ -private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRef stx do +private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRef stx $ withMainMVarContext do let usingRecStx := stx[2] let withAlts := stx[4] if usingRecStx.isNone then diff --git a/tests/lean/run/inductionTacticBug.lean b/tests/lean/run/inductionTacticBug.lean new file mode 100644 index 0000000000..9455bc5cfd --- /dev/null +++ b/tests/lean/run/inductionTacticBug.lean @@ -0,0 +1,6 @@ +def ex {α} : Subsingleton (Squash α) := Subsingleton.intro $ by + intro a b + induction a using Squash.ind + induction b using Squash.ind + apply Quot.sound + exact trivial