Commit eb74aeab authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix error messages for iSplitL/iSplitR.

parent f2a278d5
......@@ -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:
......
......@@ -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.
......
......@@ -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
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment