Commit 857f9909 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make solve_ndisj more powerful.

It now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.
parent 7b36d0e4
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 613168bf8af3af0fe31873efd89038a89800792e
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 3103b7bf52d0275f2938d9af44ab2d0db89a6251
......@@ -95,4 +95,8 @@ Hint Extern 1 (_ ⊆ _) => apply nclose_subseteq' : ndisj.
Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
Hint Resolve ndisj_difference_l : ndisj.
Ltac solve_ndisj := solve [eauto with ndisj].
Ltac solve_ndisj :=
repeat match goal with
| H : _ _ _ |- _ => apply union_subseteq in H as [??]
end;
solve [eauto with ndisj].
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