diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index bccbbcf852f231ef8622b878e92c25d7621b0234..8efdfd4af7148eaa7c7b5b25addacc2fc668d54d 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1464,9 +1464,10 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
     | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
     | ESelIdent ?p ?H :: ?Hs =>
        iRevert H; go Hs;
-       let H' :=
-         match p with true => constr:([IAlwaysElim (IIdent H)]) | false => H end in
-       iIntros H'
+       match p with
+       | true => iIntro #H
+       | false => iIntro H
+       end
     end in
   try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.