diff --git a/iris/proofmode/intro_patterns.v b/iris/proofmode/intro_patterns.v
index 4847e2aca14d192056a36eaa6c9e7090ec6120b6..b111915492176140c332e007c2badbc21798fe3b 100644
--- a/iris/proofmode/intro_patterns.v
+++ b/iris/proofmode/intro_patterns.v
@@ -136,23 +136,32 @@ Ltac parse s :=
   | intro_pat => constr:([s])
   | list string =>
      lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
-     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
+     | Some ?pats => pats
+     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
      end
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
+     | Some ?pats => pats
+     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
      end
   | ident => constr:([IIdent s])
-  | ?X => fail "intro_pat.parse:" s "has unexpected type" X
+  | ?X => fail "intro_pat.parse: the term" s
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 Ltac parse_one s :=
   lazymatch type of s with
   | intro_pat => s
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some [?pat] => pat | _ => fail "intro_pat.parse_one: cannot parse" s
+     | Some [?pat] => pat
+     | _ => fail "intro_pat.parse_one: cannot parse" s "as an introduction pattern"
      end
-  | ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
+  | ?X => fail "intro_pat.parse_one: the term" s
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End intro_pat.
 
@@ -176,5 +185,8 @@ Ltac intro_pat_intuitionistic p :=
      eval cbv in (forallb intro_pat_intuitionistic pat)
   | ident => false
   | bool => p
-  | ?X => fail "intro_pat_intuitionistic:" p "has unexpected type" X
+  | ?X => fail "intro_pat_intuitionistic: the term" p
+     "is expected to be an introduction pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
diff --git a/iris/proofmode/sel_patterns.v b/iris/proofmode/sel_patterns.v
index 6f498a36560fd998624152ebf123f497ff1bdfa2..ea736320cc7ec8d4185e91bc8951ad7bd695f26a 100644
--- a/iris/proofmode/sel_patterns.v
+++ b/iris/proofmode/sel_patterns.v
@@ -37,7 +37,12 @@ Ltac parse s :=
   | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
   | string =>
      lazymatch eval vm_compute in (parse s) with
-     | Some ?pats => pats | _ => fail "invalid sel_pat" s
+     | Some ?pats => pats
+     | _ => fail "sel_pat.parse: cannot parse" s "as a selection pattern"
      end
+  | ?X => fail "sel_pat.parse: the term" s
+     "is expected to be a selection pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End sel_pat.
diff --git a/iris/proofmode/spec_patterns.v b/iris/proofmode/spec_patterns.v
index 983b6d260479db08838c0de29ca30e22ba54b9df..7b8032343969ae78590c0be911f6fda53a6ae1f4 100644
--- a/iris/proofmode/spec_patterns.v
+++ b/iris/proofmode/spec_patterns.v
@@ -92,10 +92,15 @@ Ltac parse s :=
   lazymatch type of s with
   | list spec_pat => s
   | spec_pat => constr:([s])
-  | string => lazymatch eval vm_compute in (parse s) with
-              | Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
-              end
+  | string =>
+     lazymatch eval vm_compute in (parse s) with
+     | Some ?pats => pats
+     | _ => fail "spec_pat.parse: cannot parse" s "as a specialization pattern"
+     end
   | ident => constr:([SIdent s []])
-  | ?X => fail "spec_pat.parse:" s "has unexpected type" X
+  | ?X => fail "spec_pat.parse: the term" s
+     "is expected to be a specialization pattern"
+     "(usually a string),"
+     "but has unexpected type" X
   end.
 End spec_pat.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 4e422856398f825dcab94426321f0e0fa8c07998..745fd6013a47f59042da695487b48049636f9ec3 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -727,6 +727,18 @@ The command has indeed failed with message:
 Tactic failure: 
 "Only non-mask-changing update modalities can be introduced directly.
 Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
+"iRevert_wrong_sel_pat"
+     : string
+The command has indeed failed with message:
+Tactic failure: sel_pat.parse: the term n
+is expected to be a selection pattern (usually a string),
+but has unexpected type nat.
+"iInduction_wrong_sel_pat"
+     : string
+The command has indeed failed with message:
+Tactic failure: sel_pat.parse: the term m
+is expected to be a selection pattern (usually a string),
+but has unexpected type nat.
 "test_pure_name"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 71fabc8ba821bf9442acc0962f8aa3b749ffcbcc..454da8ec78f183803c0c52ad445b845eb3884553 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1435,6 +1435,20 @@ Proof.
   Fail iIntros "!>".
 Abort.
 
+Check "iRevert_wrong_sel_pat".
+Lemma iRevert_wrong_sel_pat (n m : nat) (P Q : nat → PROP) :
+  ⌜ n = m ⌝ -∗ P n -∗ P m.
+Proof.
+  Fail iRevert n.
+Abort.
+
+Check "iInduction_wrong_sel_pat".
+Lemma iInduction_wrong_sel_pat (n m : nat) (P Q : nat → PROP) :
+  ⌜ n = m ⌝ -∗ P n -∗ P m.
+Proof.
+  Fail iInduction n as [|n] "IH" forall m.
+Abort.
+
 End error_tests.
 
 Section pure_name_tests.