From 2472f932c13e0e00b08eb1e00c2fcaaf78b260a8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 16 Dec 2016 14:55:12 +0100
Subject: [PATCH] make ndisj hints look through definitions to unfold more
 stuff

---
 theories/base_logic/lib/namespaces.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index 58819d812..0b958278f 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -88,8 +88,8 @@ of the forms:
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
 Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
-Hint Resolve ndot_preserve_disjoint_l : ndisj.
-Hint Resolve ndot_preserve_disjoint_r : ndisj.
+Hint Extern 1 (_ ⊥ _) => apply ndot_preserve_disjoint_l : ndisj.
+Hint Extern 1 (_ ⊥ _) => apply ndot_preserve_disjoint_r : ndisj.
 Hint Extern 1 (_ ⊆ _) => apply nclose_subseteq' : ndisj.
 Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
 Hint Resolve ndisj_difference_l : ndisj.
-- 
GitLab