From 078ec73d98c538a25b569f24a5af6078ec653fe8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Feb 2017 12:57:27 +0100
Subject: [PATCH] add eauto hint Db for calling solve_ndisj

---
 theories/base_logic/lib/namespaces.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index d1f987623..ccbe3d063 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -100,3 +100,4 @@ Ltac solve_ndisj :=
   | H : _ ∪ _ ⊆ _ |- _ => apply union_subseteq in H as [??]
   end;
   solve [eauto with ndisj].
+Hint Extern 1000 => solve_ndisj : solve_ndisj.
-- 
GitLab