Merge branch 'ralf/max_prefix_list' into 'master'

unstage max_prefix_list

See merge request !705

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`:**
 

_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

iris_staging/algebra/max_prefix_list.v → iris/algebra/max_prefix_list.v

-(* 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.

iris_staging/algebra/mono_list.v

 (* 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.