From 4891e581850836e3701605565a0e268023226a74 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 Aug 2023 17:59:46 +0200
Subject: [PATCH] Move MRA out of unstable.
---
_CoqProject | 2 +-
iris_unstable/algebra/monotone.v => iris/algebra/mra.v | 4 ----
tests/{monotone.ref => mra.ref} | 0
tests/{monotone.v => mra.v} | 2 +-
4 files changed, 2 insertions(+), 6 deletions(-)
rename iris_unstable/algebra/monotone.v => iris/algebra/mra.v (97%)
rename tests/{monotone.ref => mra.ref} (100%)
rename tests/{monotone.v => mra.v} (90%)
diff --git a/_CoqProject b/_CoqProject
index cbad09513..0a078486a 100644
--- a/_CoqProject
+++ b/_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
diff --git a/iris_unstable/algebra/monotone.v b/iris/algebra/mra.v
similarity index 97%
rename from iris_unstable/algebra/monotone.v
rename to iris/algebra/mra.v
index 0439b9fe2..8e67bcd4f 100644
--- a/iris_unstable/algebra/monotone.v
+++ b/iris/algebra/mra.v
@@ -1,7 +1,3 @@
-(** 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.
diff --git a/tests/monotone.ref b/tests/mra.ref
similarity index 100%
rename from tests/monotone.ref
rename to tests/mra.ref
diff --git a/tests/monotone.v b/tests/mra.v
similarity index 90%
rename from tests/monotone.v
rename to tests/mra.v
index 061f57872..fff618361 100644
--- a/tests/monotone.v
+++ b/tests/mra.v
@@ -1,5 +1,5 @@
From stdpp Require Import propset gmap strings.
-From iris.unstable.algebra Require Import monotone.
+From iris Require Import algebra.mra.
Unset Mangle Names.
--
GitLab