diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index b818f7d0cfd86da1219838a459cf4e674858ce46..53c6708799b3287ed165dee9e084afb34f36c956 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1250,6 +1250,7 @@ Ltac iHypsContaining x :=
 Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
   iRevertIntros Hs with (
     iRevertIntros "∗" with (
+      idtac;
       let Hsx := iHypsContaining x in
       iRevertIntros Hsx with tac
     )