diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2d055b316e33133b587bcad2b8dad9fd511abb53..41293ccd01bc6364c4ee5c9ba3808917b7f71a9e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1032,7 +1032,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
      | true =>
         iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
      | false =>
-        iPoseProofCoreLem t as Htmp before_tc (spec_tac ()); [..|tac Htmp]
+        iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
      end
   end.