From 646bfc85e7ea6313e62feecf4ebcbcd76a186e71 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 May 2017 22:57:53 +0200
Subject: [PATCH] Oops, forgot that.

---
 theories/proofmode/tactics.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index b818f7d0c..53c670879 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
     )
-- 
GitLab