From 857f9909b773754d521d47f0fe6f43aec6c3214d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2017 21:47:02 +0100
Subject: [PATCH] Make solve_ndisj more powerful.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.
---
 opam.pins                            | 2 +-
 theories/base_logic/lib/namespaces.v | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/opam.pins b/opam.pins
index 45f895921..64a42bfc6 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 613168bf8af3af0fe31873efd89038a89800792e
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 3103b7bf52d0275f2938d9af44ab2d0db89a6251
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index a1b7774ce..d1f987623 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -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].
-- 
GitLab