diff git a/tests/proofmode.ref b/tests/proofmode.ref
index 9e44b1d373876221954769b0ad982cfbc3b2b9b8..307e797b204b4be894c7d176bb7400c356a58fbd 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 f1b43337b65f11f4110fb8c0de3429d0ef03bb23..be62f71209eb4454cb2957dacb74e67bab963af0 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.