From a9ebd97277f2688f08efcded717e2593fd44a361 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 29 Nov 2021 18:02:23 -0500
Subject: [PATCH] unstage mono_list algebra

---
 _CoqProject                                          |  2 +-
 .../algebra => iris/algebra/lib}/mono_list.v         | 12 ++++--------
 iris_staging/base_logic/mono_list.v                  |  2 +-
 3 files changed, 6 insertions(+), 10 deletions(-)
 rename {iris_staging/algebra => iris/algebra/lib}/mono_list.v (97%)

diff --git a/_CoqProject b/_CoqProject
index 985d186bf..0847d523a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,6 +55,7 @@ iris/algebra/lib/ufrac_auth.v
 iris/algebra/lib/dfrac_agree.v
 iris/algebra/lib/gmap_view.v
 iris/algebra/lib/mono_nat.v
+iris/algebra/lib/mono_list.v
 iris/algebra/lib/gset_bij.v
 iris/si_logic/siprop.v
 iris/si_logic/bi.v
@@ -174,7 +175,6 @@ iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
 
 iris_staging/algebra/list.v
-iris_staging/algebra/mono_list.v
 iris_staging/base_logic/algebra.v
 iris_staging/base_logic/mono_list.v
 iris_staging/heap_lang/interpreter.v
diff --git a/iris_staging/algebra/mono_list.v b/iris/algebra/lib/mono_list.v
similarity index 97%
rename from iris_staging/algebra/mono_list.v
rename to iris/algebra/lib/mono_list.v
index ee2468dd7..df5e68c4c 100644
--- a/iris_staging/algebra/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -1,13 +1,9 @@
-(* This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/439 for details on remaining
-issues before stabilization. *)
-From iris.algebra Require Export auth dfrac max_prefix_list.
-From iris.algebra Require Import updates local_updates proofmode_classes.
-From iris.prelude Require Import options.
-
 (** Authoritative CMRA of append-only lists, where the fragment represents a
   snap-shot of the list, and the authoritative element can only grow by
   appending. *)
+From iris.algebra Require Export auth dfrac max_prefix_list.
+From iris.algebra Require Import updates local_updates proofmode_classes.
+From iris.prelude Require Import options.
 
 Definition mono_listR (A : ofe) : cmra  := authR (max_prefix_listUR A).
 Definition mono_listUR (A : ofe) : ucmra  := authUR (max_prefix_listUR A).
@@ -192,7 +188,7 @@ Section mono_list_props.
   (** * Update *)
   Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 → ●ML l1 ~~> ●ML l2.
   Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
-  Lemma mono_list_update_auth_persist dq l : ●ML{dq} l ~~> ●□ML l.
+  Lemma mono_list_auth_persist dq l : ●ML{dq} l ~~> ●□ML l.
   Proof.
     rewrite /mono_list_auth. apply cmra_update_op; [|done].
     by apply auth_update_auth_persist.
diff --git a/iris_staging/base_logic/mono_list.v b/iris_staging/base_logic/mono_list.v
index 642a7a1a7..f410dd857 100644
--- a/iris_staging/base_logic/mono_list.v
+++ b/iris_staging/base_logic/mono_list.v
@@ -16,7 +16,7 @@ which allows one to grow the auth element by appending only. At any time the
 auth list can be "snapshotted" with [mono_list_lb_own_get] to produce a
 persistent lower-bound. *)
 From iris.proofmode Require Import tactics.
-From iris.staging.algebra Require Import mono_list.
+From iris.algebra.lib Require Import mono_list.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
-- 
GitLab