Bad error message when `mintro` fails to parse

[david-christiansen]

Description

mintro is implemented in two parts: there is a macro available without imports that throws an error that directs users to the correct import, and a full implementation that takes precedence with the import present. Unfortunately, with the import present, the other error message can still be triggered, leading to confusing error messages.

Steps to Reproduce

Use this code:

import Std.Do
import Std.Tactic.Do

open Std.Do

def bump (n : Nat) : StateM Nat Nat := do
  modify (· + n)
  get

theorem bump_correct : ⦃ fun n => ⌜n = k⌝ ⦄ bump m ⦃ ⇓ r n => ⌜r = n ∧ n = k + m⌝  ⦄ := by
  mstart
  mintro

Expected behavior:

I would expect an error message related to mintro requiring an argument.

Actual behavior:
I get this error:

to use `mintro`, please include `import Std.Tactic.Do`

Versions

Lean 4.27.0-nightly-2025-11-30

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[sgraf812]

Presumably this is because the full implementation requires at least one argument:

@[tactic_alt Lean.Parser.Tactic.mintroMacro]
syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic

Will look into this soon.