make empty operational typeclass TC opaque

Like iris!914 (merged), but only for the Empty typeclass which (being just a constant) is particularly prone to Coq TC instance "hallucination".

stdpp/base.v

@@ -962,6 +962,9 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Global Hint Mode Empty ! : typeclass_instances.
 Notation "∅" := empty (format "∅") : stdpp_scope.
+(** [empty] as a mere constant is particularly prone to Coq just making up instances when no real instance can be found;
+this is prevented by making the projection opaque for TC resolution. *)
+Global Typeclasses Opaque empty.
 
 Global Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.