From 46d8457afc0ae9d347f22e8421faf858b4bfb42a Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 22 Nov 2021 13:00:20 -0500 Subject: [PATCH] update append-only list tracking issue --- iris_staging/algebra/mono_list.v | 2 +- iris_staging/base_logic/mono_list.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/iris_staging/algebra/mono_list.v b/iris_staging/algebra/mono_list.v index c1f6b4b15..ee2468dd7 100644 --- a/iris_staging/algebra/mono_list.v +++ b/iris_staging/algebra/mono_list.v @@ -1,5 +1,5 @@ (* This file is still experimental. See its tracking issue -https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining +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. diff --git a/iris_staging/base_logic/mono_list.v b/iris_staging/base_logic/mono_list.v index 7fba7b74e..642a7a1a7 100644 --- a/iris_staging/base_logic/mono_list.v +++ b/iris_staging/base_logic/mono_list.v @@ -1,5 +1,5 @@ (* This file is still experimental. See its tracking issue -https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining +https://gitlab.mpi-sws.org/iris/iris/-/issues/439 for details on remaining issues before stabilization. *) (** Ghost state for a append-only list, wrapping the [mono_listR] RA. This provides three assertions: -- GitLab