Commit 5bd2042e authored by Robbert Krebbers's avatar Robbert Krebbers

Handle ⊣⊢ consistently in iProof instead of iSplit.

parent 66320c79
...@@ -47,6 +47,7 @@ Tactic Notation "iProof" := ...@@ -47,6 +47,7 @@ Tactic Notation "iProof" :=
| |- of_envs _ _ => fail "iProof: already in Iris proofmode" | |- of_envs _ _ => fail "iProof: already in Iris proofmode"
| |- True _ => apply tac_adequate | |- True _ => apply tac_adequate
| |- _ _ => apply uPred.wand_entails, tac_adequate | |- _ _ => apply uPred.wand_entails, tac_adequate
| |- _ _ => apply uPred.iff_equiv, tac_adequate
end. end.
(** * Context manipulation *) (** * Context manipulation *)
...@@ -508,12 +509,12 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) := ...@@ -508,12 +509,12 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
(** * Conjunction and separating conjunction *) (** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" := Tactic Notation "iSplit" :=
try iProof;
lazymatch goal with lazymatch goal with
| |- _ _ => | |- _ _ =>
eapply tac_and_split; eapply tac_and_split;
[let P := match goal with |- FromAnd ?P _ _ => P end in [let P := match goal with |- FromAnd ?P _ _ => P end in
apply _ || fail "iSplit:" P "not a conjunction"| |] apply _ || fail "iSplit:" P "not a conjunction"| |]
| |- _ _ => apply (anti_symm ())
end. end.
Tactic Notation "iSplitL" constr(Hs) := Tactic Notation "iSplitL" constr(Hs) :=
......
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