From b470f38b0d063a534691059fa2a637e7124a6ce7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 14 Jun 2021 12:31:18 +0200
Subject: [PATCH] Add tests.

---
 tests/proofmode.ref |  8 ++++++++
 tests/proofmode.v   | 14 ++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 4e4228563..bee3ca0f4 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 71fabc8ba..454da8ec7 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.
-- 
GitLab