From f133c8cd3623cfa12755c99247f892c3247cf3cc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Nov 2019 15:17:17 +0100
Subject: [PATCH] Move derived `auth` algebra stuff in `lib` folder.

---
 _CoqProject                             | 6 +++---
 theories/algebra/{ => lib}/excl_auth.v  | 0
 theories/algebra/{ => lib}/frac_auth.v  | 0
 theories/algebra/{ => lib}/ufrac_auth.v | 0
 theories/base_logic/lib/boxes.v         | 2 +-
 theories/heap_lang/lib/counter.v        | 2 +-
 theories/program_logic/ownp.v           | 2 +-
 7 files changed, 6 insertions(+), 6 deletions(-)
 rename theories/algebra/{ => lib}/excl_auth.v (100%)
 rename theories/algebra/{ => lib}/frac_auth.v (100%)
 rename theories/algebra/{ => lib}/ufrac_auth.v (100%)

diff --git a/_CoqProject b/_CoqProject
index 4a568257d..e361d046c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,8 +17,6 @@ theories/algebra/big_op.v
 theories/algebra/cmra_big_op.v
 theories/algebra/sts.v
 theories/algebra/auth.v
-theories/algebra/frac_auth.v
-theories/algebra/excl_auth.v
 theories/algebra/gmap.v
 theories/algebra/ofe.v
 theories/algebra/base.v
@@ -40,7 +38,9 @@ theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
 theories/algebra/namespace_map.v
-theories/algebra/ufrac_auth.v
+theories/algebra/lib/excl_auth.v
+theories/algebra/lib/frac_auth.v
+theories/algebra/lib/ufrac_auth.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
diff --git a/theories/algebra/excl_auth.v b/theories/algebra/lib/excl_auth.v
similarity index 100%
rename from theories/algebra/excl_auth.v
rename to theories/algebra/lib/excl_auth.v
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/lib/frac_auth.v
similarity index 100%
rename from theories/algebra/frac_auth.v
rename to theories/algebra/lib/frac_auth.v
diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
similarity index 100%
rename from theories/algebra/ufrac_auth.v
rename to theories/algebra/lib/ufrac_auth.v
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 7b205e54b..bf478327c 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import excl_auth gmap agree.
+From iris.algebra Require Import lib.excl_auth gmap agree.
 From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 8dfe67e62..1d0fd7083 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac_auth auth.
+From iris.algebra Require Import lib.frac_auth auth.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 17469f957..85109f320 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics classes.
-From iris.algebra Require Import excl_auth.
+From iris.algebra Require Import lib.excl_auth.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
-- 
GitLab