Add tests.

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

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.