diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index df2cc9712695a348b65241118b0cc74435b34347..c04c2b4a9e5d125424f0df847c5429a492674d21 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -472,6 +472,16 @@ Tactic failure: iSplitR: hypotheses ["HPx"] not found.
 The command has indeed failed with message:
 Ltac call to "iSplitR (constr)" failed.
 Tactic failure: iSplitR: hypotheses ["HPx"] not found.
+"iSplitL_non_splittable"
+     : string
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: P not a separating conjunction.
+"iSplitR_non_splittable"
+     : string
+The command has indeed failed with message:
+Ltac call to "iSplitR (constr)" failed.
+Tactic failure: iSplitR: P not a separating conjunction.
 "iCombine_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 07af70c40f1bc7f1d439e3d07f9c7986a5822042..54f4663b516486ca15b44d4586c2efe183fb516e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -791,6 +791,20 @@ Proof.
   iIntros "HP1 HP2". Fail iSplitR "HP1 HPx". Fail iSplitR "HPx HP1".
 Abort.
 
+Check "iSplitL_non_splittable".
+Lemma iSplitL_non_splittable P :
+  P.
+Proof.
+  Fail iSplitL "".
+Abort.
+
+Check "iSplitR_non_splittable".
+Lemma iSplitR_non_splittable P :
+  P.
+Proof.
+  Fail iSplitR "".
+Abort.
+
 Check "iCombine_fail".
 Lemma iCombine_fail P:
   P -∗ P -∗ P ∗ P.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index b349b89140ead7624471ec63e6ff9efa17cb5c28..b8fd465302fe6cb3f642ca3bc4fdf68df6be9f86 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1135,7 +1135,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
   let Δ := iGetCtx in
   eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
     [iSolveTC ||
-     let P := match goal with |- FromSep _ ?P _ _ => P end in
+     let P := match goal with |- FromSep ?P _ _ => P end in
      fail "iSplitL:" P "not a separating conjunction"
     |pm_reduce;
      lazymatch goal with
@@ -1151,7 +1151,7 @@ Tactic Notation "iSplitR" constr(Hs) :=
   let Δ := iGetCtx in
   eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *)
     [iSolveTC ||
-     let P := match goal with |- FromSep _ ?P _ _ => P end in
+     let P := match goal with |- FromSep ?P _ _ => P end in
      fail "iSplitR:" P "not a separating conjunction"
     |pm_reduce;
      lazymatch goal with