From 7b5e32b96e352fb37ab1496ca51599e3837f185c Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 10 Mar 2020 09:29:03 -0400
Subject: [PATCH] Avoid using Hint Resolve with a term

This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.
---
 theories/coPset.v     |  3 ++-
 theories/namespaces.v | 18 ++++++++++++------
 2 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/theories/coPset.v b/theories/coPset.v
index 92fb2974..4048edf4 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -185,7 +185,8 @@ Proof.
 Qed.
 
 (** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
-Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
+Local Definition coPset_top_subseteq := top_subseteq (C:=coPset).
+Hint Resolve coPset_top_subseteq : core.
 
 Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 04f9e931..c135f3bb 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -78,11 +78,15 @@ Create HintDb ndisj.
 (** Rules for goals of the form [_ ⊆ _] *)
 (** If-and-only-if rules. Well, not quite, but for the fragment we are
 considering they are. *)
-Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
-Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
-Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
+Local Definition coPset_subseteq_difference_r := subseteq_difference_r (C:=coPset).
+Hint Resolve coPset_subseteq_difference_r : ndisj.
+Local Definition coPset_empty_subseteq := empty_subseteq (C:=coPset).
+Hint Resolve coPset_empty_subseteq : ndisj.
+Local Definition coPset_union_least := union_least (C:=coPset).
+Hint Resolve coPset_union_least : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
-Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
+Local Definition coPset_subseteq_difference_l := subseteq_difference_l (C:=coPset).
+Hint Resolve coPset_subseteq_difference_l | 100 : ndisj.
 Hint Resolve nclose_subseteq' | 100 : ndisj.
 
 (** Rules for goals of the form [_ ## _] *)
@@ -90,8 +94,10 @@ Hint Resolve nclose_subseteq' | 100 : ndisj.
 Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress.
 Tests show trying [disjoint_difference_l1] first gives better performance. *)
-Hint Resolve (disjoint_difference_l1 (A:=positive) (C:=coPset)) | 50 : ndisj.
-Hint Resolve (disjoint_difference_l2 (A:=positive) (C:=coPset)) | 100 : ndisj.
+Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset).
+Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
+Local Definition coPset_disjoint_difference_l2 := disjoint_difference_l2 (C:=coPset).
+Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
 Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
 
 Ltac solve_ndisj :=
-- 
GitLab