diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 958f3a16466870d3e1209b19f99ee29f02899557..8efc6955bd06a234eaeb87f49cf070e7f840953d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -644,6 +644,7 @@ Local Tactic Notation "iForallRevert" ident(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 ?Δ (∀ y, @?P y) =>
          change (envs_entails Δ (∀ x, P x)); lazy beta
@@ -676,7 +677,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.