diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 7ff16dd1523a0252c962c5547972c16765d0ce51..b0eb97b17523053ae7f2c51214adcaf7da2f811d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -639,9 +639,19 @@ Local Tactic Notation "iForallRevert" ident(x) :=
   lazymatch type of A with
   | Prop =>
      revert x; first
-       [eapply tac_pure_revert; [tc_solve (* [FromAffinely], should never fail *)|]
+       [eapply tac_pure_revert;
+         [tc_solve (* [FromAffinely], should never fail *)
+         |]
        |err x]
-  | _ => revert x; first [apply tac_forall_revert|err x]
+  | _ =>
+    revert x; first
+      [apply tac_forall_revert;
+       (* Ensure the name [x] is preserved, see [test_iRevert_order_and_names]. *)
+       lazymatch goal with
+       | |- envs_entails ?Δ (bi_forall ?P) =>
+         change (envs_entails Δ (∀ x, P x)); lazy beta
+       end
+      |err x]
   end.
 
 (** The tactic [iRevertHyp H with tac] reverts the hypothesis [H] and calls
@@ -669,7 +679,10 @@ Tactic Notation "iRevert" constr(Hs) :=
        go Hs
     | ESelIdent _ ?H :: ?Hs => iRevertHyp H; go Hs
     end in
-  iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
+  iStartProof;
+  let Hs := iElaborateSelPat Hs in
+  (* No need to reverse [Hs], [iElaborateSelPat] already does that. *)
+  go Hs.
 
 Tactic Notation "iRevert" "(" ident(x1) ")" :=
   iForallRevert x1.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 5d08d96a13d9b1feecf948cc4dee3cbc312dc230..480eb6486ef855f2895f0d2512e11c904788eca4 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -628,6 +628,14 @@ No applicable tactic.
   "H" : <affine> ⌜φ⌝ -∗ P
   --------------------------------------∗
   <affine> ⌜φ⌝ -∗ P
+"test_iRevert_order_and_names"
+     : string
+1 goal
+  
+  PROP : bi
+  ============================
+  --------------------------------------∗
+  ∀ P1 P2, P1 -∗ P2 -∗ P1 ∗ P2
 "test_iRevert_pure_affine"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9dec1daa99436b5b81803357d6dce5187183eff9..e78302a57fd3e9d545b2577f58cfdc782d188165 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1433,6 +1433,16 @@ Proof.
   iIntros (Hφ) "H". iRevert (Hφ). Show. done.
 Qed.
 
+Check "test_iRevert_order_and_names".
+Lemma test_iRevert_order_and_names P1 P2 : P1 -∗ P2 -∗ P1 ∗ P2.
+Proof.
+  iIntros "H1 H2". iRevert (P1 P2) "H1 H2".
+  (* Check that the reverts are performed in the right order (i.e., reverse),
+  and that the names [P1] and [P2] are used in the goal. *)
+  Show.
+  auto with iFrame.
+Qed.
+
 Check "test_iRevert_pure_affine".
 Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
   φ → (⌜ φ ⌝ -∗ P) -∗ P.