From dca0b2500b3c9cb9d348a1ac215fec65728bf91e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 5 Jun 2019 19:14:54 +0200
Subject: [PATCH] docs: for now we won't document atomic triples or total
 triples; de-experimentalize plainly and stuckness

---
 CHANGELOG.md  | 6 +++---
 docs/iris.tex | 6 +-----
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 18b28cab9..9a6df74fb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,9 +14,9 @@ Changes in and extensions of the theory:
 * [#] Weaken the semantics of CAS in heap_lang to be efficiently implementable:
   CAS may only be used to compare "unboxed" values that can be represented in a
   single machine word.
-* [#] Add weakest preconditions for total program correctness.
-* [#] "(Potentially) stuck" weakest preconditions are no longer considered
-  experimental.
+* Add weakest preconditions for total program correctness.
+* "(Potentially) stuck" weakest preconditions and the "plainly modality" are no
+  longer considered experimental.
 * The adequacy statement for weakest preconditions now also involves the
   final state.
 * [#] Add the notion of an "observation" to the language interface, so that
diff --git a/docs/iris.tex b/docs/iris.tex
index bd5792b41..c227a50d6 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -40,11 +40,7 @@ For further information, visit the Iris project website at \url{http://plv.mpi-s
 \section{Iris from the Ground Up}
 In \citetitle{iris-ground-up}~\cite{iris-ground-up}, we describe Iris~3.1 in a bottom-up way.
 That paper is hence much more suited as an introduction to the model of Iris than this reference, which mostly contains definitions, not explanations or examples.
-The following differences between Iris as described in \citetitle{iris-ground-up} and the latest version documented here are worth mentioning:
-\begin{itemize}
-\item As an experimental feature, we added the \emph{plainly modality} $\plainly$.
-\item As an experimental feature, weakest preconditions take a \emph{stuckness} $\stuckness$ as parameter, indicating whether the program may get stuck or not.
-\end{itemize}
+For a list of changes in Iris since then, please consult \href{https://gitlab.mpi-sws.org/iris/iris/blob/master/CHANGELOG.md}{our changelog}.
 \endgroup
 
 \clearpage\begingroup
-- 
GitLab