From f870cdaf91bacb0403b715e6a268754882ea868d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Mar 2017 14:07:41 +0100
Subject: [PATCH] actually create the ndisj HintDb. this makes it unfold
 constants so that we can use 'Hint Resolve'.

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

diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index ccbe3d063..d806f9eed 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -87,13 +87,12 @@ of the forms:
 - [N1 ⊥ N2] 
 - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
+Create HintDb ndisj.
 Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : 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 ndot_preserve_disjoint_l ndot_preserve_disjoint_r
+     nclose_subseteq' ndisj_difference_l : ndisj.
 Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
-Hint Resolve ndisj_difference_l : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with
-- 
GitLab