Add a bunch of test cases for `iRevert`.

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".

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.