Includes deprecation warning

leanprover · Aug 5, 2024 · a8683f2 · a8683f2
1 parent 49242e0
commit a8683f2
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -416,7 +416,9 @@ macro "sorry" : tactic => `(tactic| exact @sorryAx _ false)
 
 /-- `admit` is a shorthand for `exact sorry`. -/
 @[deprecated (since := "2024-08-04")]
-macro "admit" : tactic => `(tactic| exact @sorryAx _ false)
+macro "admit" : tactic => `(tactic|
+    (run_tac logWarning "`admit` is deprecated and will be removed in the future. Use `sorry` instead!"
+     exact @sorryAx _ false))
 
 /--
 `infer_instance` is an abbreviation for `exact inferInstance`.