From a21e0bafcafe0cc979d07b9216acde4ac5d04a01 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Jan 2020 14:21:18 +0100
Subject: [PATCH] Disclaimer for STSs.
---
theories/algebra/sts.v | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 410c9fef7..f4c0eb82b 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 {
--
GitLab