From 508a1c8cda4840e1e902dc6d21ec634097e6d1d8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 12 Nov 2020 13:59:54 +0100
Subject: [PATCH] move algebra.base -> prelude.prelude
---
_CoqProject | 2 +-
iris/algebra/ofe.v | 2 +-
iris/{algebra/base.v => prelude/prelude.v} | 0
iris/program_logic/ectx_language.v | 2 +-
iris/program_logic/ectxi_language.v | 2 +-
iris/proofmode/base.v | 2 +-
iris/proofmode/environments.v | 2 +-
iris_heap_lang/locations.v | 2 +-
8 files changed, 7 insertions(+), 7 deletions(-)
rename iris/{algebra/base.v => prelude/prelude.v} (100%)
diff --git a/_CoqProject b/_CoqProject
index 598e82936..ecff6175e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,6 +15,7 @@
-arg -w -arg -redundant-canonical-projection
iris/prelude/options.v
+iris/prelude/prelude.v
iris/algebra/monoid.v
iris/algebra/cmra.v
iris/algebra/big_op.v
@@ -25,7 +26,6 @@ iris/algebra/view.v
iris/algebra/auth.v
iris/algebra/gmap.v
iris/algebra/ofe.v
-iris/algebra/base.v
iris/algebra/dra.v
iris/algebra/cofe_solver.v
iris/algebra/agree.v
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 135865d7e..87f734ef5 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
Set Primitive Projections.
diff --git a/iris/algebra/base.v b/iris/prelude/prelude.v
similarity index 100%
rename from iris/algebra/base.v
rename to iris/prelude/prelude.v
diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index a76f590ed..df53a0185 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -1,6 +1,6 @@
(** An axiomatization of evaluation-context based languages, including a proof
that this gives rise to a "language" in the Iris sense. *)
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
From iris.program_logic Require Import language.
From iris.prelude Require Import options.
diff --git a/iris/program_logic/ectxi_language.v b/iris/program_logic/ectxi_language.v
index e3a245b2e..bbb6d9052 100644
--- a/iris/program_logic/ectxi_language.v
+++ b/iris/program_logic/ectxi_language.v
@@ -1,6 +1,6 @@
(** An axiomatization of languages based on evaluation context items, including
a proof that these are instances of general ectx-based languages. *)
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
From iris.program_logic Require Import language ectx_language.
From iris.prelude Require Import options.
diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index 5a969fea0..0c9168eeb 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -1,6 +1,6 @@
From Coq Require Export Ascii.
From stdpp Require Export strings.
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
(** * Utility definitions used by the proofmode *)
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index e185690dc..fb132f827 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
From iris.bi Require Export bi.
From iris.proofmode Require Import base.
From iris.prelude Require Import options.
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index 7cca50788..6da303478 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -1,5 +1,5 @@
From stdpp Require Import countable numbers gmap.
-From iris.algebra Require Import base.
+From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
Record loc := { loc_car : Z }.
--
GitLab