Merge branch 'robbert/mra' into 'master'

Move MRA out of unstable.

Closes #414

See merge request iris/iris!963

CHANGELOG.md

@@ -50,6 +50,9 @@ Coq 8.13 is no longer supported.
 * Rename `singleton_mono` to `singleton_included_mono`.
 * Use `Strategy expand` for CMRA/UCMRA coercions and most projections to improve
   performance of type-checking some large CMRA/OFE types. (by Ike Mulder)
+* Add monotone resource algebra, `algebra/mra.v`, to enable reasoning about
+  monotonicity with respect to an arbitrary preorder relation: the extension order
+  of `mra R` is designed to embed the preorder relation `R`. (by Amin Timany)
 
 **Changes in `bi`:**
 

_CoqProject

@@ -50,6 +50,7 @@ iris/algebra/ufrac.v
 iris/algebra/reservation_map.v
 iris/algebra/dyn_reservation_map.v
 iris/algebra/max_prefix_list.v
+iris/algebra/mra.v
 iris/algebra/lib/excl_auth.v
 iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v
@@ -187,7 +188,6 @@ iris_unstable/algebra/list.v
 iris_unstable/base_logic/algebra.v
 iris_unstable/base_logic/mono_list.v
 iris_unstable/heap_lang/interpreter.v
-iris_unstable/algebra/monotone.v
 
 iris_deprecated/base_logic/auth.v
 iris_deprecated/base_logic/sts.v

iris_unstable/algebra/monotone.v → iris/algebra/mra.v

-(** This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/414 for details on remaining
-issues before stabilization. *)
-
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Import options.

tests/monotone.v → tests/mra.v

 From stdpp Require Import propset gmap strings.
-From iris.unstable.algebra Require Import monotone.
+From iris Require Import algebra.mra.
 
 Unset Mangle Names.