diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 4e422856398f825dcab94426321f0e0fa8c07998..bee3ca0f48bebeeeb2d20540d0657991c703cac1 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -727,6 +727,14 @@ 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: n has unexpected type nat.
+"iInduction_wrong_sel_pat"
+     : string
+The command has indeed failed with message:
+Tactic failure: sel_pat.parse: m 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.