Commit 8ca3fc9b authored by Robbert Krebbers's avatar Robbert Krebbers

Make iSplit work on goals of the shape ⊣⊢.

parent bbec6617
......@@ -333,9 +333,13 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
eapply tac_and_split;
[let P := match goal with |- AndSplit ?P _ _ => P end in
apply _ || fail "iSplit:" P "not a conjunction"| |].
lazymatch goal with
| |- _ _ =>
eapply tac_and_split;
[let P := match goal with |- AndSplit ?P _ _ => P end in
apply _ || fail "iSplit:" P "not a conjunction"| |]
| |- _ ⊣⊢ _ => apply (anti_symm ())
end.
Tactic Notation "iSplitL" constr(Hs) :=
let Hs := words Hs in
......
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