From bf1737e28b3bd919a0f1642b137c2eb1bf44976a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Jun 2021 20:39:36 +0200
Subject: [PATCH] unstage max_prefix_list
---
CHANGELOG.md | 2 ++
_CoqProject | 2 +-
{iris_staging => iris}/algebra/max_prefix_list.v | 6 +++---
iris_staging/algebra/mono_list.v | 3 +--
4 files changed, 7 insertions(+), 6 deletions(-)
rename {iris_staging => iris}/algebra/max_prefix_list.v (97%)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 607fdf3d9..bea7aca77 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,8 @@ Coq 8.11 is no longer supported in this version of Iris.
algorithm.
* Set `Hint Mode` for the classes `OfeDiscrete`, `Unit`, `CmraMorphism`,
`rFunctorContractive`, `urFunctorContractive`.
+* Add `max_prefix_list` RA on lists whose composition is only defined when one
+ operand is a prefix of the other. The result is the longer list.
**Changes in `bi`:**
diff --git a/_CoqProject b/_CoqProject
index 1ec070191..b21005506 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -46,6 +46,7 @@ iris/algebra/proofmode_classes.v
iris/algebra/ufrac.v
iris/algebra/reservation_map.v
iris/algebra/dyn_reservation_map.v
+iris/algebra/max_prefix_list.v
iris/algebra/lib/excl_auth.v
iris/algebra/lib/frac_auth.v
iris/algebra/lib/ufrac_auth.v
@@ -170,7 +171,6 @@ iris_heap_lang/lib/arith.v
iris_heap_lang/lib/array.v
iris_staging/algebra/list.v
-iris_staging/algebra/max_prefix_list.v
iris_staging/algebra/mono_list.v
iris_staging/base_logic/algebra.v
iris_staging/base_logic/mono_list.v
diff --git a/iris_staging/algebra/max_prefix_list.v b/iris/algebra/max_prefix_list.v
similarity index 97%
rename from iris_staging/algebra/max_prefix_list.v
rename to iris/algebra/max_prefix_list.v
index 30f35f7c2..3643c1d83 100644
--- a/iris_staging/algebra/max_prefix_list.v
+++ b/iris/algebra/max_prefix_list.v
@@ -1,6 +1,6 @@
-(* This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
-issues before stabilization. *)
+(** Defines an RA on lists whose composition is only defined when one operand is
+a prefix of the other. The result is the longer list.
+In particular, the core is the identity function for all elements. *)
From iris.algebra Require Export agree list gmap updates.
From iris.algebra Require Import local_updates proofmode_classes.
From iris.prelude Require Import options.
diff --git a/iris_staging/algebra/mono_list.v b/iris_staging/algebra/mono_list.v
index a41715451..c1f6b4b15 100644
--- a/iris_staging/algebra/mono_list.v
+++ b/iris_staging/algebra/mono_list.v
@@ -1,8 +1,7 @@
(* This file is still experimental. See its tracking issue
https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
issues before stabilization. *)
-From iris.algebra Require Export auth dfrac.
-From iris.staging.algebra Require Export max_prefix_list.
+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.
--
GitLab