diff --git a/theories/listset.v b/theories/listset.v
index 00872d02efc7058c8ec7d7b32846eeeb5b22dd81..5aa61a4cd498b79ba180fc597a76f49d2fd1bcf1 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -16,6 +16,7 @@ Instance listset_empty: Empty (listset A) := Listset [].
 Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
 Instance listset_union: Union (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (l' ++ k').
+Global Opaque listset_singleton listset_empty.
 
 Global Instance: SimpleCollection A (listset A).
 Proof.