From 9b1cb0559f397a7b359bd1cb1ad88caf2294ccdb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 12 Aug 2019 13:02:29 +0200
Subject: [PATCH] Add a bunch of test cases for `iRevert`.

---
 tests/proofmode.ref | 38 ++++++++++++++++++++++++++++++++++++++
 tests/proofmode.v   | 20 +++++++++++++++++++-
 2 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 9e44b1d37..307e797b2 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -668,3 +668,41 @@ In nested Ltac calls to "iApply (open_constr)",
 failed.
 Tactic failure: iApply: Q
 not absorbing and the remaining hypotheses not affine.
+"iRevert_wrong_var"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) )" and 
+"iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k1 not in scope.
+The command has indeed failed with message:
+In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
+"iLöbRevert (constr) with (tactic3)",
+"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
+"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
+"∗" with tac), "iRevertIntros (constr) with (tactic3)", 
+"iRevertIntros_go", "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as
+IH), "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
+"iRevertIntros ( (ident) ) (constr) with (tactic3)",
+"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
+"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )), 
+"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
+"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k1 not in scope.
+"iRevert_dup_var"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) (ident) )",
+"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k not in scope.
+"iRevert_dep_var_coq"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) )", "iForallRevert (ident)" and
+"revert (ne_var_list)", last call failed.
+k is used in hypothesis Hk.
+"iRevert_dep_var"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) )" and 
+"iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k is used in hypothesis "Hk".
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f1b43337b..be62f7120 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -684,7 +684,6 @@ Lemma test_iDestruct_clear P Q R :
 Proof.
   iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
 Qed.
-
 End tests.
 
 (** Test specifically if certain things print correctly. *)
@@ -909,4 +908,23 @@ Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.
 Check "iApply_fail_not_affine_2".
 Lemma iApply_fail_not_affine_1 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
 Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
+
+Check "iRevert_wrong_var".
+Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : Φ (S k).
+Proof.
+  Fail iRevert (k1).
+  Fail iLöb as "IH" forall (k1).
+Abort.
+
+Check "iRevert_dup_var".
+Lemma iRevert_dup_var (k : nat) (Φ : nat → PROP) : Φ (S k).
+Proof. Fail iRevert (k k). Abort.
+
+Check "iRevert_dep_var_coq".
+Lemma iRevert_dep_var_coq (k : nat) (Φ : nat → PROP) : k = 0 → Φ (S k).
+Proof. intros Hk. Fail iRevert (k). Abort.
+
+Check "iRevert_dep_var".
+Lemma iRevert_dep_var (k : nat) (Φ : nat → PROP) : Φ k -∗ Φ (S k).
+Proof. iIntros "Hk". Fail iRevert (k). Abort.
 End error_tests.
-- 
GitLab