From f1a4f71c13d9c20da836b9d492f6950e1c1d9f8c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 23 Jul 2021 10:22:57 +0200
Subject: [PATCH] prefer Hint Resolve over Hint Extern

---
 theories/namespaces.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/namespaces.v b/theories/namespaces.v
index 3c0f1b19..975d7f48 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -111,8 +111,11 @@ Global Hint Extern 10 (_ ## (_ ∖ _)) =>
   end : ndisj.
 (** Before we apply disjoint_difference, let's make sure we normalize the goal
 to [_ ∖ (_ ∪ _)]. *)
-Global Hint Extern 20 ((?X ∖ ?Y ∖ ?Z) ## _) =>
-  rewrite (difference_difference_L (C:=coPset) X Y Z) : ndisj.
+Local Lemma coPset_difference_difference (X1 X2 X3 Y : coPset) :
+  X1 ∖ (X2 ∪ X3) ## Y →
+  X1 ∖ X2 ∖ X3 ## Y.
+Proof. set_solver. Qed.
+Global Hint Resolve coPset_difference_difference | 20 : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress.
 Tests show trying [disjoint_difference_l1] first gives better performance. *)
 Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset).
-- 
GitLab