diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 603e332535916ea9a8fafabf80786178df8ed54e..ce14c1f7d0d7931aa99c503f9c2b60657d5bc3ef 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1053,29 +1053,38 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
   iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "∗" with (iLöbCore as IH).
 
 Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1) Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")"
     constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1 x2) Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x3) ")" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1 x2 x3) Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x3) ident(x4) ")" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1 x2 x3 x4) Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x3) ident(x4) ident(x5) ")" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1 x2 x3 x4 x5) Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x3) ident(x4) ident(x5) ident(x6) ")" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1 x2 x3 x4 x5 x6) Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1 x2 x3 x4 x5 x6 x7) Hs with (iLöbCore as IH).
 Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
+  let Hs := constr:(Hs +:+ "∗") in
   iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iLöbCore as IH).
 
 (** * Assert *)