From 6c7b99c2dd261fb7e67a339da89bdb12a3189678 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 27 Nov 2017 13:57:16 +0100
Subject: [PATCH] docs: this is Iris 3.1
---
CHANGELOG.md | 2 +-
docs/iris.tex | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index ca6541a89..baa924f03 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,7 +7,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
Changes in and extensions of the theory:
-* [#] Add new modality: â– ("plainly").
+* Add new modality: â– ("plainly").
* Camera morphisms have to be homomorphisms, not just monotone functions.
* Add a proof that `f` has a fixed point if `f^k` is contractive.
* Constructions for least and greatest fixed points over monotone predicates
diff --git a/docs/iris.tex b/docs/iris.tex
index 83d56c6d7..dfe6a1dbc 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -16,7 +16,7 @@
\input{setup}
-\title{\bfseries The Iris 3.0 Documentation}
+\title{\bfseries The Iris 3.1 Documentation}
\author{\url{http://plv.mpi-sws.org/iris/}}
--
GitLab