Commit 6c7b99c2 authored by Ralf Jung's avatar Ralf Jung
Browse files

docs: this is Iris 3.1

parent 31598b91
......@@ -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
......@@ -16,7 +16,7 @@
\title{\bfseries The Iris 3.0 Documentation}
\title{\bfseries The Iris 3.1 Documentation}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment