[Backport releases/v4.8.0] fix: rfl tactic error messsage when there …

…are no goals (#4068) Backport 26a1b93 from #4067. Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
leanprover · May 5, 2024 · 4961ee1 · 4961ee1
1 parent 02753f6
commit 4961ee1
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -368,7 +368,7 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
 Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")

diff --git a/tests/lean/run/issue4063.lean b/tests/lean/run/issue4063.lean
@@ -0,0 +1,5 @@
+/-- error: no goals to be solved -/
+#guard_msgs in
+example : 3 = 3 := by
+  rfl
+  rfl