Enable solve_ndisj to handle unions on the LHS.

7dec931b · Robbert Krebbers · e906ef70 · 7dec931b
Commit 7dec931b authored Mar 28, 2017 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 2 deletions

theories/base_logic/lib/namespaces.v theories/base_logic/lib/namespaces.v +3 -2

No files found.
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -90,10 +90,11 @@ of the forms:
 Create HintDb ndisj.
 Hint Resolve ndisj_subseteq_difference : ndisj.
 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 ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
+Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
 Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
 Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
+Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.

 Ltac solve_ndisj :=
  repeat match goal with