diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 6b0b0c1c8f79e941abfe36b1b8dcdad63dba880a..cc6bac66fdb0dbde4197adab07e000c83f2a3617 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -648,6 +648,10 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
     ident(x11) ident(x12) ident(x13) ident(x14) ")" :=
   iForallRevert x14; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
+    ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" :=
+  iForallRevert x15; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
 
 Tactic Notation "iRevert" "(" ident(x1) ")" constr(Hs) :=
   iRevert Hs; iRevert ( x1 ).
@@ -693,6 +697,10 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
     ident(x11) ident(x12) ident(x13) ident(x14) ")" constr(Hs) :=
   iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
+    ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
+  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ).
 
 (** * The specialize and pose proof tactics *)
 Record iTrm {X As S} :=
@@ -1512,6 +1520,13 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
     simple_intropattern(x9) simple_intropattern(x10) simple_intropattern(x11)
     simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14) ")" :=
   iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ); iIntro ( x14 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8)
+    simple_intropattern(x9) simple_intropattern(x10) simple_intropattern(x11)
+    simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14)
+    simple_intropattern(x15) ")" :=
+  iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ); iIntro ( x15 ).
 
 Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" constr(p) :=
   iIntros ( x1 ); iIntros p.
@@ -1576,6 +1591,13 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
     simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14)
     ")" constr(p) :=
   iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ); iIntros p.
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8)
+    simple_intropattern(x9) simple_intropattern(x10) simple_intropattern(x11)
+    simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14)
+    simple_intropattern(x15) ")" constr(p) :=
+  iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ); iIntros p.
 
 Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1) ")" :=
   iIntros p; iIntros ( x1 ).
@@ -1640,6 +1662,13 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
     simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
     simple_intropattern(x14) ")" :=
   iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
+Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10)
+    simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
+    simple_intropattern(x14) simple_intropattern(x15) ")" :=
+  iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ).
 
 Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1) ")" constr(p2) :=
   iIntros p; iIntros ( x1 ); iIntros p2.
@@ -1708,6 +1737,13 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
     simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
     simple_intropattern(x14) ")" constr(p2) :=
   iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ); iIntros p2.
+Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10)
+    simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
+    simple_intropattern(x14) simple_intropattern(x15) ")" constr(p2) :=
+  iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x15 ); iIntros p2.
 
 (* Used for generalization in iInduction and iLöb *)
 Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
@@ -1775,6 +1811,11 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x12) ident(x13) ident(x14) ")" constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14);
     tac; iIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)).
+Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10) ident(x11)
+    ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) "with" tactic3(tac):=
+  iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x14);
+    tac; iIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)).
 
 Tactic Notation "iRevertIntros" "with" tactic3(tac) :=
   iRevertIntros "" with tac.
@@ -1823,6 +1864,10 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10) ident(x11)
     ident(x12) ident(x13) ident(x14) ")" "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with tac.
+Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10) ident(x11)
+    ident(x12) ident(x13) ident(x14) ident(x15) ")" "with" tactic3(tac):=
+  iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with tac.
 
 (** * Destruct tactic *)
 Class CopyDestruct {PROP : bi} (P : PROP).
@@ -2114,6 +2159,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
   iInductionRevert x "" with
     (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
       (iInductionCore (induction x as pat) as IH)).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
+    ident(x7) ident(x8) ident (x9) ident(x10) ident(x11) ident(x12) ident(x13)
+    ident(x14) ident(x15) ")" :=
+  iInductionRevert x "" with
+    (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
+      (iInductionCore (induction x as pat) as IH)).
 
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "forall" constr(Hs) :=
@@ -2195,6 +2247,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
   iInductionRevert x Hs with
     (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
       (iInductionCore (induction x as pat) as IH)).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
+    ident(x7) ident(x8) ident (x9) ident(x10) ident(x11) ident(x12) ident(x13)
+    ident(x14) ident(x15) ")" constr(Hs) :=
+  iInductionRevert x Hs with
+    (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
+      (iInductionCore (induction x as pat) as IH)).
 
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) :=
@@ -2279,6 +2338,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
   iInductionRevert x "" with
     (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
       (iInductionCore (induction x as pat using u) as IH)).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) ident (x9) ident(x10) ident(x11)
+    ident(x12) ident(x13) ident(x14) ident(x15) ")" :=
+  iInductionRevert x "" with
+    (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
+      (iInductionCore (induction x as pat using u) as IH)).
 
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) "forall" constr(Hs) :=
@@ -2362,6 +2428,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
   iInductionRevert x Hs with
     (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
       (iInductionCore (induction x as pat using u) as IH)).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) ident (x9) ident(x10) ident(x11)
+    ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
+  iInductionRevert x Hs with
+    (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
+      (iInductionCore (induction x as pat using u) as IH)).
 
 (** * Löb Induction *)
 Tactic Notation "iLöbCore" "as" constr (IH) :=
@@ -2437,6 +2510,11 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ")" :=
   iLöbRevert "" with
     (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" 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) ident(x9)
+    ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" :=
+  iLöbRevert "" with
+    (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with (iLöbCore as IH)).
 
 Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
   iLöbRevert Hs with (iLöbCore as IH).
@@ -2492,6 +2570,11 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
     ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ")" constr(Hs) :=
   iLöbRevert Hs with
     (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" 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) ident(x9)
+    ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
+  iLöbRevert Hs with
+    (iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with (iLöbCore as IH)).
 
 (** * Assert *)
 (* The argument [p] denotes whether [Q] is persistent. It can either be a