Different error message for copied tactic

Stream: metaprogramming / tactics

[Jon Eugster]

What goes wrong here? I thought I could just copy-paste the rewrite tactic into my project (for now without any modification), but if I do so, it works as expected except that it does not show the error message "unknown identifier" anymore.

Why does this happen? The only difference in the code should be that one is a builtin_tactic and one is a tactic...

import Lean.Elab.Tactic.Rewrite

namespace Lean.Elab.Tactic
open Meta
open Lean.Parser.Tactic

/- From Lean Core:

```
syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
```

and

```
@[builtin_tactic Lean.Parser.Tactic.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
  let cfg ← elabRewriteConfig stx[1]
  let loc   := expandOptLocation stx[3]
  withRWRulesSeq stx[0] stx[2] fun symm term => do
    withLocation loc
      (rewriteLocalDecl term symm · cfg)
      (rewriteTarget term symm cfg)
      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
```

-/

example (a b : Nat) : a * b = b * a := by
  rewrite [mul_comm] -- has `unknonwn identifier`

syntax (name := _root_.MyProject.rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic

@[tactic _root_.MyProject.rewriteSeq] def _root_.MyProject.evalRewriteSeq : Tactic := fun stx => do
  let cfg ← elabRewriteConfig stx[1]
  let loc   := expandOptLocation stx[3]
  withRWRulesSeq stx[0] stx[2] fun symm term => do
    withLocation loc
      (rewriteLocalDecl term symm · cfg)
      (rewriteTarget term symm cfg)
      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")

example (a b : Nat) : a * b = b * a := by
  rewrite [mul_comm] -- does not have `unknown identifier`