From ccddd0d9323b0598dec052098001dacd6ffef471 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Jan 2022 16:22:08 -0800 Subject: [PATCH] feat: show proof state/unclosed goal message on empty tactic sequences closes #361 --- src/Lean/Elab/Tactic/Basic.lean | 3 ++- tests/361.lean | 5 +++++ tests/lean/361.lean.expected.out | 1 + 3 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 tests/361.lean create mode 100644 tests/lean/361.lean.expected.out diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 030b0f5a6d..7bdc1ffd4b 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -175,7 +175,7 @@ mutual expandTacticMacroFns stx (macroAttribute.getEntries (← getEnv) stx.getKind) partial def evalTacticAux (stx : Syntax) : TacticM Unit := - withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with + withRef stx <| withIncRecDepth <| withFreshMacroScope $ match stx with | Syntax.node _ k args => if k == nullKind then -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]` @@ -186,6 +186,7 @@ mutual match tacticElabAttribute.getEntries (← getEnv) stx.getKind with | [] => expandTacticMacro stx | evalFns => evalTacticUsing s stx evalFns + | Syntax.missing => pure () | _ => throwError m!"unexpected tactic{indentD stx}" partial def evalTactic (stx : Syntax) : TacticM Unit := diff --git a/tests/361.lean b/tests/361.lean new file mode 100644 index 0000000000..afe69af83e --- /dev/null +++ b/tests/361.lean @@ -0,0 +1,5 @@ +theorem ex1 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by + +theorem ex2 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by + cases h1 + case inl => diff --git a/tests/lean/361.lean.expected.out b/tests/lean/361.lean.expected.out new file mode 100644 index 0000000000..59ab0eb12c --- /dev/null +++ b/tests/lean/361.lean.expected.out @@ -0,0 +1 @@ +file '361.lean' not found