diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 410c9fef72d84ad525b7066d179bbdd681232f41..f4c0eb82bfe12839af1d1bc2c4e91149d6577562 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -6,6 +6,12 @@ Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
 
+(** DISCLAIMER: The definition of STSs is included in the Iris development for
+historical purposes. If you plan to mechanize an Iris proof in Coq, it is
+usually better to use a more direct encoding of the ghost state you need as a
+resource algebra (camera). STSs are very painful to use in Coq, and they are
+therefore barely used in practice. *)
+
 (** * Definition of STSs *)
 Module sts.
 Structure stsT := Sts {