From 318ef8823ae474aa723c47bfaade33ac78b380ff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Sep 2017 20:22:28 +0200
Subject: [PATCH] Make algebra/proofmode_classes.v no longer depend on
base_logic.
---
_CoqProject | 2 +-
theories/algebra/auth.v | 3 ++-
theories/algebra/frac.v | 2 +-
theories/algebra/frac_auth.v | 2 +-
theories/{base_logic => algebra}/proofmode_classes.v | 2 +-
theories/base_logic/lib/own.v | 2 +-
theories/base_logic/proofmode.v | 2 +-
7 files changed, 8 insertions(+), 7 deletions(-)
rename theories/{base_logic => algebra}/proofmode_classes.v (96%)
diff --git a/_CoqProject b/_CoqProject
index deeba1135..8f1e85df3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,6 +24,7 @@ theories/algebra/local_updates.v
theories/algebra/gset.v
theories/algebra/coPset.v
theories/algebra/deprecated.v
+theories/algebra/proofmode_classes.v
theories/bi/interface.v
theories/bi/derived.v
theories/bi/big_op.v
@@ -39,7 +40,6 @@ theories/base_logic/soundness.v
theories/base_logic/double_negation.v
theories/base_logic/deprecated.v
theories/base_logic/proofmode.v
-theories/base_logic/proofmode_classes.v
theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 07cff4db7..607d0cae2 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,5 +1,6 @@
From iris.algebra Require Export excl local_updates.
-From iris.base_logic Require Import base_logic proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
+From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type".
Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 253ceae52..d76652cc9 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,6 +1,6 @@
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
Notation frac := Qp (only parsing).
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 1d564f3ac..92de4e235 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export frac auth.
From iris.algebra Require Export updates local_updates.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
Definition frac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR fracR A)).
diff --git a/theories/base_logic/proofmode_classes.v b/theories/algebra/proofmode_classes.v
similarity index 96%
rename from theories/base_logic/proofmode_classes.v
rename to theories/algebra/proofmode_classes.v
index e24217f6c..1c033303b 100644
--- a/theories/base_logic/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,5 +1,5 @@
From iris.proofmode Require Export classes.
-From iris.base_logic Require Export base_logic.
+From iris.algebra Require Export cmra.
(* There are various versions of [IsOp] with different modes:
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 308331a04..b4d220326 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import iprod gmap.
From iris.base_logic.lib Require Export iprop.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
Import uPred.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index ac7c11bef..40f79a6a7 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -1,6 +1,6 @@
From iris.base_logic Require Export base_logic.
From iris.proofmode Require Export tactics.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
Import uPred.
Import bi.
--
GitLab