Oops, forgot that.

646bfc85 · Robbert Krebbers · a64bb337 · 646bfc85
Commit 646bfc85 authored May 12, 2017 by Robbert Krebbers
--- 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
    )