From 1f223f8f5f4b28be6566bc2434b9cc88be6a688d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 19 Feb 2020 11:37:38 +0100
Subject: [PATCH] Put `top_subseteq` in core DB to fix Iris regression.

---
 theories/namespaces.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/namespaces.v b/theories/namespaces.v
index 67f7447a..4cd3092d 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -80,12 +80,15 @@ Create HintDb ndisj.
 considering they are. *)
 Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
-Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
 Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
 Hint Resolve nclose_subseteq' | 100 : ndisj.
 
+(** Put this hint in [core] so that only only [solve_ndisj], but also [done] and
+friends, can solve trivial goals of the form [E ⊆ ⊤] that occur often. *)
+Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
+
 (** Rules for goals of the form [_ ## _] *)
 (** The base rule that we want to ultimately get down to. *)
 Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
-- 
GitLab