From d6474135baac39a271c301a17d6621691a48b80b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 19 Apr 2024 07:30:51 +0200
Subject: [PATCH] feat: upstream false_or_by_contra tests (#3947)

And fix broken `builtin_tactic` attribute.
---
 src/Lean/Elab/Tactic/FalseOrByContra.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/FalseOrByContra.lean b/src/Lean/Elab/Tactic/FalseOrByContra.lean
index e3967607cb..7e03d23244 100644
--- a/src/Lean/Elab/Tactic/FalseOrByContra.lean
+++ b/src/Lean/Elab/Tactic/FalseOrByContra.lean
@@ -58,7 +58,7 @@ partial def falseOrByContra (g : MVarId) (useClassical : Option Bool := none) :
       let [g] ← g.applyConst ``False.elim | panic! "expected one sugoal"
       pure g
 
-@[builtin_tactic falseOrByContra]
+@[builtin_tactic Lean.Parser.Tactic.falseOrByContra]
 def elabFalseOrByContra : Tactic
    | `(tactic| false_or_by_contra) => do liftMetaTactic1 (falseOrByContra ·)
    | _ => no_error_if_unused% throwUnsupportedSyntax