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

@@ -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.