Merge branch 'joe/fix_iSplit_errors' into 'master'

Fix error messages for iSplitL/iSplitR.

See merge request iris/iris!261

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:

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.

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