Enable solve_ndisj to solve `∅ ⊆ X`.

3d6525a5 · Robbert Krebbers · 69653240 · 3d6525a5 · 3d6525a5
Commit 3d6525a5 authored Mar 15, 2017 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

opam.pins opam.pins +1 -1

theories/base_logic/lib/namespaces.v theories/base_logic/lib/namespaces.v +1 -0

No files found.
--- a/opam.pins
+++ b/opam.pins
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 36363712499dbdf7a4cd2acf91877787b839c79a
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp fd8a6717a2610c00dec920ee5f33b00b14ef1fbf
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -93,6 +93,7 @@ Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r
     nclose_subseteq' ndisj_difference_l : ndisj.
 Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
+Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.

 Ltac solve_ndisj :=
  repeat match goal with