From eb74aeabd313c95f5f70770dccf57e373c6e0b65 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Sun, 9 Jun 2019 15:33:48 -0400
Subject: [PATCH] Fix error messages for iSplitL/iSplitR.

---
 tests/proofmode.ref               | 10 ++++++++++
 tests/proofmode.v                 | 14 ++++++++++++++
 theories/proofmode/ltac_tactics.v |  4 ++--
 3 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index df2cc9712..c04c2b4a9 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 07af70c40..54f4663b5 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 b349b8914..b8fd46530 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
-- 
GitLab