diff --git a/stdpp/base.v b/stdpp/base.v
index 9eda10f5ee7bb32bb652d43c5083491704440ae1..9fa9c168ec693652bb7c67be87934fff72bc39cf 100644
--- a/stdpp/base.v
+++ b/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 ∅.