diff --git a/.gitignore b/.gitignore
index bfd0941de270424fc4efa0ae01ac97992a86ca9d..fead3cd9c1980bbefe11706d32bd576c5e722dce 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,7 +4,6 @@
*.vio
*.v.d
.coqdeps.d
-.Makefile.coq.d
*.glob
*.cache
*.aux
@@ -14,8 +13,12 @@
*.bak
.coqdeps.d
.coq-native/
+*.crashcoqide
+.env
builddep/
+_CoqProject.*
Makefile.coq
Makefile.coq.conf
-*.crashcoqide
-.env
+.Makefile.coq.d
+Makefile.package.*
+.Makefile.package.*
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8e82fc715fe3aba030ed7dba48d010ea4911b6c0..414e1f503212fe9f1e4d2cc4be16076cc8afe3eb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -37,7 +37,7 @@ build-coq.8.12.0:
variables:
OPAM_PINS: "coq version 8.12.0"
DENY_WARNINGS: "1"
- OPAM_PKG: "coq-iris"
+ OPAM_PKG: "1"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
tags:
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 93c63457d4938ee0cf79099e96d621bc207f2810..75e420e68e2629617ccfa636f720bce5a8fdb2db 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,9 @@ lemma.
With this release, we dropped support for Coq 8.9.
+We also split Iris into multiple opam packages: `coq-iris` no longer contains
+HeapLang, which is now in a separate package `coq-iris-heap-lang`.
+
**Changes in `algebra`:**
* Rename `agree_op_inv'` to `to_agree_op_inv`,
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 67eef817ff135946e050e0ed2e2544af05b7ace0..39e074c325fae1e95a3a51a0cd7b9d16cad7f2cc 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -5,6 +5,23 @@ Iris development. This is for contributing to Iris itself; see
[the README](README.md#further-resources) for resources helpful for all Iris
users.
+To work on Iris itself, you need to install its build-dependencies. Again we
+recommend you do that with opam (2.0.0 or newer). This requires the following
+two repositories:
+
+ opam repo add coq-released https://coq.inria.fr/opam/released
+ opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+
+Once you got opam set up, run `make build-dep` to install the right versions
+of the dependencies.
+
+Run `make -jN` to build the full development, where `N` is the number of your
+CPU cores.
+
+To update Iris, do `git pull`. After an update, the development may fail to
+compile because of outdated dependencies. To fix that, please run `opam update`
+followed by `make build-dep`.
+
## How to submit a merge request
To contribute code, you need an [MPI-SWS GitLab account][account] (use the
@@ -48,6 +65,20 @@ Coq-8.8-specific `.ref` file). If you change one of these, remember to update
If you want to compile without tests run `make NO_TEST=1`.
+## How to build/install only one package
+
+Iris is split into multiple packages that can be installed separately via opam.
+You can invoke the Makefile of a particular package by doing `./make-package
+$PACKAGE $MAKE_ARGS`, where `$MAKE_ARGS` are passed to `make` (so you can use
+the usual `-jN`, `install`, ...). This should only rarely be necessary. For
+example, if you are not using opam and you want to install only the `iris`
+package (without HeapLang, to avoid waiting on that part of the build), you can
+do `./make-package iris install`. (If you are using opam, you can achieve the
+same by pinning `coq-iris` to your Iris checkout.)
+
+Note that `./make-package` will never run the test suite, so please always do a
+regular `make -jN` before submitting an MR.
+
## How to measure the timing effect on a reverse dependency
So say you did a change in Iris, and want to know how it affects [lambda-rust]
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 9ff769d27a157fdad62aec46b89e87bf50cc93e7..4d24c334ba2b121802ea34f0dce1fdaf490e9fbe 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -14,7 +14,7 @@ NORMALIZER:=test-normalizer.sed
test: $(TESTFILES:.v=.vo)
# Make sure everything imports the options.
$(HIDE)for FILE in $(VFILES); do \
- if ! fgrep -q 'From iris Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi \
+ if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi \
done
.PHONY: test
diff --git a/README.md b/README.md
index bb35b8274154d10963fdd8f8612cb9233c48d163..3b38ae5c476bf7e1631d07d141560f8639c0eaf5 100644
--- a/README.md
+++ b/README.md
@@ -50,34 +50,24 @@ To obtain a development version, also add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-Either way, you can now do `opam install coq-iris`. To fetch updates later, run
-`opam update && opam upgrade`. However, notice that we do not guarantee
-backwards-compatibility, so upgrading Iris may break your Iris-using
-developments.
-
-The development version of Iris is regularly subject to breaking changes. If
-you want to be notified of such changes, please let us know your account name on
-the [MPI-SWS GitLab](https://gitlab.mpi-sws.org/) so we can add you to the
+Either way, you can now install Iris:
+- `opam install coq-iris` will install the libraries making up the Iris logic,
+ but leave it up to you to instantiate the `program_logic.language` interface
+ to define a programming language for Iris to reason about.
+- `opam install coq-iris-heap-lang` will additionally install HeapLang, the
+ default language used by various Iris projects.
+
+To fetch updates later, run `opam update && opam upgrade`. However, notice that
+we do not guarantee backwards-compatibility, so upgrading Iris may break your
+Iris-using developments. If you want to be notified of breaking changes, please
+let us know your account name on the
+[MPI-SWS GitLab](https://gitlab.mpi-sws.org/) so we can add you to the
notification group.
### Working *on* Iris
-To work on Iris itself, you need to install its build-dependencies. Again we
-recommend you do that with opam (2.0.0 or newer). This requires the following
-two repositories:
-
- opam repo add coq-released https://coq.inria.fr/opam/released
- opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-
-Once you got opam set up, run `make build-dep` to install the right versions
-of the dependencies.
-
-Run `make -jN` to build the full development, where `N` is the number of your
-CPU cores.
-
-To update Iris, do `git pull`. After an update, the development may fail to
-compile because of outdated dependencies. To fix that, please run `opam update`
-followed by `make build-dep`.
+See the [contribution guide](CONTRIBUTING.md) for information on how to work on
+the Iris development itself.
## Directory Structure
diff --git a/_CoqProject b/_CoqProject
index 37fc08f79110c9c5fe5e6184b586ae78a2361ec7..598e82936d254ab21ad1d2030f603a210e92a06e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,155 +1,165 @@
--Q theories iris
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q iris/prelude iris.prelude
+-Q iris/algebra iris.algebra
+-Q iris/si_logic iris.si_logic
+-Q iris/bi iris.bi
+-Q iris/proofmode iris.proofmode
+-Q iris/base_logic iris.base_logic
+-Q iris/program_logic iris.program_logic
+-Q iris_heap_lang iris.heap_lang
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-theories/options.v
-theories/algebra/monoid.v
-theories/algebra/cmra.v
-theories/algebra/big_op.v
-theories/algebra/cmra_big_op.v
-theories/algebra/sts.v
-theories/algebra/numbers.v
-theories/algebra/view.v
-theories/algebra/auth.v
-theories/algebra/gmap.v
-theories/algebra/ofe.v
-theories/algebra/base.v
-theories/algebra/dra.v
-theories/algebra/cofe_solver.v
-theories/algebra/agree.v
-theories/algebra/excl.v
-theories/algebra/functions.v
-theories/algebra/frac.v
-theories/algebra/dfrac.v
-theories/algebra/csum.v
-theories/algebra/list.v
-theories/algebra/vector.v
-theories/algebra/updates.v
-theories/algebra/local_updates.v
-theories/algebra/gset.v
-theories/algebra/gmultiset.v
-theories/algebra/coPset.v
-theories/algebra/proofmode_classes.v
-theories/algebra/ufrac.v
-theories/algebra/namespace_map.v
-theories/algebra/lib/excl_auth.v
-theories/algebra/lib/frac_auth.v
-theories/algebra/lib/ufrac_auth.v
-theories/algebra/lib/frac_agree.v
-theories/algebra/lib/gmap_view.v
-theories/algebra/lib/mnat_auth.v
-theories/si_logic/siprop.v
-theories/si_logic/bi.v
-theories/bi/notation.v
-theories/bi/interface.v
-theories/bi/derived_connectives.v
-theories/bi/derived_laws.v
-theories/bi/derived_laws_later.v
-theories/bi/plainly.v
-theories/bi/internal_eq.v
-theories/bi/big_op.v
-theories/bi/updates.v
-theories/bi/ascii.v
-theories/bi/bi.v
-theories/bi/monpred.v
-theories/bi/embedding.v
-theories/bi/weakestpre.v
-theories/bi/telescopes.v
-theories/bi/lib/counterexamples.v
-theories/bi/lib/fixpoint.v
-theories/bi/lib/fractional.v
-theories/bi/lib/laterable.v
-theories/bi/lib/atomic.v
-theories/bi/lib/core.v
-theories/bi/lib/relations.v
-theories/base_logic/upred.v
-theories/base_logic/bi.v
-theories/base_logic/derived.v
-theories/base_logic/proofmode.v
-theories/base_logic/base_logic.v
-theories/base_logic/algebra.v
-theories/base_logic/bupd_alt.v
-theories/base_logic/lib/iprop.v
-theories/base_logic/lib/own.v
-theories/base_logic/lib/saved_prop.v
-theories/base_logic/lib/wsat.v
-theories/base_logic/lib/invariants.v
-theories/base_logic/lib/fancy_updates.v
-theories/base_logic/lib/viewshifts.v
-theories/base_logic/lib/auth.v
-theories/base_logic/lib/sts.v
-theories/base_logic/lib/boxes.v
-theories/base_logic/lib/na_invariants.v
-theories/base_logic/lib/cancelable_invariants.v
-theories/base_logic/lib/gen_heap.v
-theories/base_logic/lib/gen_inv_heap.v
-theories/base_logic/lib/fancy_updates_from_vs.v
-theories/base_logic/lib/proph_map.v
-theories/base_logic/lib/ghost_var.v
-theories/base_logic/lib/mnat.v
-theories/program_logic/adequacy.v
-theories/program_logic/lifting.v
-theories/program_logic/weakestpre.v
-theories/program_logic/total_weakestpre.v
-theories/program_logic/total_adequacy.v
-theories/program_logic/hoare.v
-theories/program_logic/language.v
-theories/program_logic/ectx_language.v
-theories/program_logic/ectxi_language.v
-theories/program_logic/ectx_lifting.v
-theories/program_logic/ownp.v
-theories/program_logic/total_lifting.v
-theories/program_logic/total_ectx_lifting.v
-theories/program_logic/atomic.v
-theories/heap_lang/locations.v
-theories/heap_lang/lang.v
-theories/heap_lang/metatheory.v
-theories/heap_lang/tactics.v
-theories/heap_lang/primitive_laws.v
-theories/heap_lang/derived_laws.v
-theories/heap_lang/notation.v
-theories/heap_lang/proofmode.v
-theories/heap_lang/adequacy.v
-theories/heap_lang/total_adequacy.v
-theories/heap_lang/proph_erasure.v
-theories/heap_lang/lib/spawn.v
-theories/heap_lang/lib/par.v
-theories/heap_lang/lib/assert.v
-theories/heap_lang/lib/lock.v
-theories/heap_lang/lib/spin_lock.v
-theories/heap_lang/lib/ticket_lock.v
-theories/heap_lang/lib/nondet_bool.v
-theories/heap_lang/lib/lazy_coin.v
-theories/heap_lang/lib/clairvoyant_coin.v
-theories/heap_lang/lib/counter.v
-theories/heap_lang/lib/atomic_heap.v
-theories/heap_lang/lib/increment.v
-theories/heap_lang/lib/diverge.v
-theories/heap_lang/lib/arith.v
-theories/heap_lang/lib/array.v
-theories/proofmode/base.v
-theories/proofmode/ident_name.v
-theories/proofmode/tokens.v
-theories/proofmode/coq_tactics.v
-theories/proofmode/ltac_tactics.v
-theories/proofmode/environments.v
-theories/proofmode/reduction.v
-theories/proofmode/intro_patterns.v
-theories/proofmode/spec_patterns.v
-theories/proofmode/sel_patterns.v
-theories/proofmode/tactics.v
-theories/proofmode/notation.v
-theories/proofmode/classes.v
-theories/proofmode/class_instances.v
-theories/proofmode/class_instances_later.v
-theories/proofmode/class_instances_updates.v
-theories/proofmode/class_instances_embedding.v
-theories/proofmode/class_instances_plainly.v
-theories/proofmode/class_instances_internal_eq.v
-theories/proofmode/frame_instances.v
-theories/proofmode/monpred.v
-theories/proofmode/modalities.v
-theories/proofmode/modality_instances.v
+iris/prelude/options.v
+iris/algebra/monoid.v
+iris/algebra/cmra.v
+iris/algebra/big_op.v
+iris/algebra/cmra_big_op.v
+iris/algebra/sts.v
+iris/algebra/numbers.v
+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
+iris/algebra/excl.v
+iris/algebra/functions.v
+iris/algebra/frac.v
+iris/algebra/dfrac.v
+iris/algebra/csum.v
+iris/algebra/list.v
+iris/algebra/vector.v
+iris/algebra/updates.v
+iris/algebra/local_updates.v
+iris/algebra/gset.v
+iris/algebra/gmultiset.v
+iris/algebra/coPset.v
+iris/algebra/proofmode_classes.v
+iris/algebra/ufrac.v
+iris/algebra/namespace_map.v
+iris/algebra/lib/excl_auth.v
+iris/algebra/lib/frac_auth.v
+iris/algebra/lib/ufrac_auth.v
+iris/algebra/lib/frac_agree.v
+iris/algebra/lib/gmap_view.v
+iris/algebra/lib/mnat_auth.v
+iris/si_logic/siprop.v
+iris/si_logic/bi.v
+iris/bi/notation.v
+iris/bi/interface.v
+iris/bi/derived_connectives.v
+iris/bi/derived_laws.v
+iris/bi/derived_laws_later.v
+iris/bi/plainly.v
+iris/bi/internal_eq.v
+iris/bi/big_op.v
+iris/bi/updates.v
+iris/bi/ascii.v
+iris/bi/bi.v
+iris/bi/monpred.v
+iris/bi/embedding.v
+iris/bi/weakestpre.v
+iris/bi/telescopes.v
+iris/bi/lib/counterexamples.v
+iris/bi/lib/fixpoint.v
+iris/bi/lib/fractional.v
+iris/bi/lib/laterable.v
+iris/bi/lib/atomic.v
+iris/bi/lib/core.v
+iris/bi/lib/relations.v
+iris/base_logic/upred.v
+iris/base_logic/bi.v
+iris/base_logic/derived.v
+iris/base_logic/proofmode.v
+iris/base_logic/base_logic.v
+iris/base_logic/algebra.v
+iris/base_logic/bupd_alt.v
+iris/base_logic/lib/iprop.v
+iris/base_logic/lib/own.v
+iris/base_logic/lib/saved_prop.v
+iris/base_logic/lib/wsat.v
+iris/base_logic/lib/invariants.v
+iris/base_logic/lib/fancy_updates.v
+iris/base_logic/lib/viewshifts.v
+iris/base_logic/lib/auth.v
+iris/base_logic/lib/sts.v
+iris/base_logic/lib/boxes.v
+iris/base_logic/lib/na_invariants.v
+iris/base_logic/lib/cancelable_invariants.v
+iris/base_logic/lib/gen_heap.v
+iris/base_logic/lib/gen_inv_heap.v
+iris/base_logic/lib/fancy_updates_from_vs.v
+iris/base_logic/lib/proph_map.v
+iris/base_logic/lib/ghost_var.v
+iris/base_logic/lib/mnat.v
+iris/program_logic/adequacy.v
+iris/program_logic/lifting.v
+iris/program_logic/weakestpre.v
+iris/program_logic/total_weakestpre.v
+iris/program_logic/total_adequacy.v
+iris/program_logic/hoare.v
+iris/program_logic/language.v
+iris/program_logic/ectx_language.v
+iris/program_logic/ectxi_language.v
+iris/program_logic/ectx_lifting.v
+iris/program_logic/ownp.v
+iris/program_logic/total_lifting.v
+iris/program_logic/total_ectx_lifting.v
+iris/program_logic/atomic.v
+iris/proofmode/base.v
+iris/proofmode/ident_name.v
+iris/proofmode/tokens.v
+iris/proofmode/coq_tactics.v
+iris/proofmode/ltac_tactics.v
+iris/proofmode/environments.v
+iris/proofmode/reduction.v
+iris/proofmode/intro_patterns.v
+iris/proofmode/spec_patterns.v
+iris/proofmode/sel_patterns.v
+iris/proofmode/tactics.v
+iris/proofmode/notation.v
+iris/proofmode/classes.v
+iris/proofmode/class_instances.v
+iris/proofmode/class_instances_later.v
+iris/proofmode/class_instances_updates.v
+iris/proofmode/class_instances_embedding.v
+iris/proofmode/class_instances_plainly.v
+iris/proofmode/class_instances_internal_eq.v
+iris/proofmode/frame_instances.v
+iris/proofmode/monpred.v
+iris/proofmode/modalities.v
+iris/proofmode/modality_instances.v
+
+iris_heap_lang/locations.v
+iris_heap_lang/lang.v
+iris_heap_lang/metatheory.v
+iris_heap_lang/tactics.v
+iris_heap_lang/primitive_laws.v
+iris_heap_lang/derived_laws.v
+iris_heap_lang/notation.v
+iris_heap_lang/proofmode.v
+iris_heap_lang/adequacy.v
+iris_heap_lang/total_adequacy.v
+iris_heap_lang/proph_erasure.v
+iris_heap_lang/lib/spawn.v
+iris_heap_lang/lib/par.v
+iris_heap_lang/lib/assert.v
+iris_heap_lang/lib/lock.v
+iris_heap_lang/lib/spin_lock.v
+iris_heap_lang/lib/ticket_lock.v
+iris_heap_lang/lib/nondet_bool.v
+iris_heap_lang/lib/lazy_coin.v
+iris_heap_lang/lib/clairvoyant_coin.v
+iris_heap_lang/lib/counter.v
+iris_heap_lang/lib/atomic_heap.v
+iris_heap_lang/lib/increment.v
+iris_heap_lang/lib/diverge.v
+iris_heap_lang/lib/arith.v
+iris_heap_lang/lib/array.v
diff --git a/coq-iris-heap-lang.opam b/coq-iris-heap-lang.opam
new file mode 100644
index 0000000000000000000000000000000000000000..7c98a1d3afad868222e43256f99aae58d5f1856a
--- /dev/null
+++ b/coq-iris-heap-lang.opam
@@ -0,0 +1,19 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+
+synopsis: "HeapLang is the canonical example language for Iris"
+description: """
+This package provides the iris.heap_lang Coq module.
+"""
+
+depends: [
+ "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_heap_lang" "-j%{jobs}%"]
+install: ["./make-package" "iris_heap_lang" "install"]
diff --git a/coq-iris.opam b/coq-iris.opam
index fd8bf766b2799a3967b10b31f49805e904a9cd6c..ec65b98decdb9eef1e82809c57b359861d6e151b 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -7,11 +7,15 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
synopsis: "Iris is a Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+description: """
+This package provides the following Coq modules:
+iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
+"""
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-10-30.0.402f2d6a") | (= "dev") }
]
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "iris" "-j%{jobs}%"]
+install: ["./make-package" "iris" "install"]
diff --git a/theories/algebra/agree.v b/iris/algebra/agree.v
similarity index 99%
rename from theories/algebra/agree.v
rename to iris/algebra/agree.v
index c0ae62c9199d1cdc0f4d30c6c57cc849314e6e86..f5733133f6b5909a69053affd9ed80561d54d3d1 100644
--- a/theories/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra.
-From iris Require Import options.
+From iris.prelude Require Import options.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
diff --git a/theories/algebra/auth.v b/iris/algebra/auth.v
similarity index 99%
rename from theories/algebra/auth.v
rename to iris/algebra/auth.v
index 6adb6c2e4f2ffe3e363b2fa599f1b55270035c39..29c5c0ae5dccc98a7213fb36edbc6d0eaa422e44 100644
--- a/theories/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export view.
From iris.algebra Require Import proofmode_classes big_op.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The authoritative camera with fractional authoritative elements *)
(** The authoritative camera has 2 types of elements: the authoritative
diff --git a/theories/algebra/base.v b/iris/algebra/base.v
similarity index 82%
rename from theories/algebra/base.v
rename to iris/algebra/base.v
index 3341e502cf497ec86ed06e360a618273c1a500c5..d915dfc3f165e0055c1527430ba5a928465a5b8b 100644
--- a/theories/algebra/base.v
+++ b/iris/algebra/base.v
@@ -1,6 +1,6 @@
From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
-From iris Require Import options.
+From iris.prelude Require Import options.
Global Open Scope general_if_scope.
Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Ltac done := stdpp.tactics.done.
diff --git a/theories/algebra/big_op.v b/iris/algebra/big_op.v
similarity index 99%
rename from theories/algebra/big_op.v
rename to iris/algebra/big_op.v
index 18c6eaa286fe5bb5b5d3ea4b79b27aa36558eeaf..92a790f25e0f988014551880b84a0ccb80846f86 100644
--- a/theories/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -1,6 +1,6 @@
From stdpp Require Export functions gmap gmultiset.
From iris.algebra Require Export monoid.
-From iris Require Import options.
+From iris.prelude Require Import options.
Local Existing Instances monoid_ne monoid_assoc monoid_comm
monoid_left_id monoid_right_id monoid_proper
monoid_homomorphism_rel_po monoid_homomorphism_rel_proper
diff --git a/theories/algebra/cmra.v b/iris/algebra/cmra.v
similarity index 99%
rename from theories/algebra/cmra.v
rename to iris/algebra/cmra.v
index cfc26604ab4b4c85c82071a6fffe0e40c56d7eae..3f8f002a1eace6db214aba9ef8ea2f824e1494f7 100644
--- a/theories/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1,6 +1,6 @@
From stdpp Require Import finite.
From iris.algebra Require Export ofe monoid.
-From iris Require Import options.
+From iris.prelude Require Import options.
Class PCore (A : Type) := pcore : A → option A.
Hint Mode PCore ! : typeclass_instances.
diff --git a/theories/algebra/cmra_big_op.v b/iris/algebra/cmra_big_op.v
similarity index 97%
rename from theories/algebra/cmra_big_op.v
rename to iris/algebra/cmra_big_op.v
index 37ae379318e422f97c87ec8f9d3a80c99c40958b..73e7d22f3322986baccbebae76861083a1267a89 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/iris/algebra/cmra_big_op.v
@@ -1,6 +1,6 @@
From stdpp Require Import gmap gmultiset.
From iris.algebra Require Export big_op cmra.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Option *)
Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
diff --git a/theories/algebra/coPset.v b/iris/algebra/coPset.v
similarity index 99%
rename from theories/algebra/coPset.v
rename to iris/algebra/coPset.v
index dcd07527b2f44ed3006152d757a4ee7d56e42a71..872cbfb87f0f20783a9ac3845a0b592fb72a2e9e 100644
--- a/theories/algebra/coPset.v
+++ b/iris/algebra/coPset.v
@@ -1,7 +1,7 @@
From stdpp Require Export sets coPset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
diff --git a/theories/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
similarity index 99%
rename from theories/algebra/cofe_solver.v
rename to iris/algebra/cofe_solver.v
index 9330d77ebb70ac11bbed9ea814fb19ebc3e1d993..948c57c220bc577b415d927161586a77641eeb8f 100644
--- a/theories/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export ofe.
-From iris Require Import options.
+From iris.prelude Require Import options.
Record solution (F : oFunctor) := Solution {
solution_car :> ofeT;
diff --git a/theories/algebra/csum.v b/iris/algebra/csum.v
similarity index 99%
rename from theories/algebra/csum.v
rename to iris/algebra/csum.v
index 74d83490b6859d6b14a4121efc8b4b15c4ce8b55..e0e5ce8fe3250fcdcbc49f37b6981ee41115bd33 100644
--- a/theories/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
-From iris Require Import options.
+From iris.prelude Require Import options.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
diff --git a/theories/algebra/dfrac.v b/iris/algebra/dfrac.v
similarity index 99%
rename from theories/algebra/dfrac.v
rename to iris/algebra/dfrac.v
index 5fadf0e77a201871c5980393a006ab5a26b9b788..4006adc937945cceddf44163622560a44321b5cf 100644
--- a/theories/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -20,7 +20,7 @@
it also implies that no one can own 1 in the future *)
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes updates frac.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** An element of dfrac denotes ownership of a fraction, knowledge that a
fraction has been discarded, or both. Note that [DfracBoth] can be written
diff --git a/theories/algebra/dra.v b/iris/algebra/dra.v
similarity index 99%
rename from theories/algebra/dra.v
rename to iris/algebra/dra.v
index 1e890200156681335fcd750d46196c99cec27e1f..5d867935846d46b2dd6cdd7adbc5c8a172ef82c0 100644
--- a/theories/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra updates.
-From iris Require Import options.
+From iris.prelude Require Import options.
Record DraMixin A `{Equiv A, PCore A, Disjoint A, Op A, Valid A} := {
(* setoids *)
diff --git a/theories/algebra/excl.v b/iris/algebra/excl.v
similarity index 99%
rename from theories/algebra/excl.v
rename to iris/algebra/excl.v
index 10a86de7442ae024fcf1dd7d1d2fc065a8cfb339..c5d9ef11007a00dfd35408a4e234a8b729383599 100644
--- a/theories/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra.
-From iris Require Import options.
+From iris.prelude Require Import options.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
diff --git a/theories/algebra/frac.v b/iris/algebra/frac.v
similarity index 98%
rename from theories/algebra/frac.v
rename to iris/algebra/frac.v
index ad8ac9ba0d91ced4853fc71a4509dbceb3dc999a..6135787f1fb0b5a9a5334a89de633d6cbdcd2d85 100644
--- a/theories/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -5,7 +5,7 @@ Notice that this camera could in principle be obtained by restricting the
validity of the unbounded fractional camera [ufrac]. *)
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Since the standard (0,1] fractional camera is used more often, we define
[frac] through a [Notation] instead of a [Definition]. That way, Coq infers the
diff --git a/theories/algebra/functions.v b/iris/algebra/functions.v
similarity index 99%
rename from theories/algebra/functions.v
rename to iris/algebra/functions.v
index dd40746ecac32593d192a3c366397d8e08ac4363..98f36dfbd6b3837c661a9c5c9fe3a7f167da903b 100644
--- a/theories/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -1,7 +1,7 @@
From stdpp Require Import finite.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT}
(x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
diff --git a/theories/algebra/gmap.v b/iris/algebra/gmap.v
similarity index 99%
rename from theories/algebra/gmap.v
rename to iris/algebra/gmap.v
index bc89495ccad60f0c4c3b67ea101c0e75bb57a253..dc39ca0feb51e4f1d2704ac2ea5c3a16d4e30277 100644
--- a/theories/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -1,7 +1,7 @@
From stdpp Require Export list gmap.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates proofmode_classes big_op.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section ofe.
Context `{Countable K} {A : ofeT}.
diff --git a/theories/algebra/gmultiset.v b/iris/algebra/gmultiset.v
similarity index 98%
rename from theories/algebra/gmultiset.v
rename to iris/algebra/gmultiset.v
index 4bbb9cf8de0cb7a9a0f5d2735813e01e37a39129..5e2f02f284b5a9cba1aec6a922b84668cd23cb80 100644
--- a/theories/algebra/gmultiset.v
+++ b/iris/algebra/gmultiset.v
@@ -1,7 +1,7 @@
From stdpp Require Export sets gmultiset countable.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates big_op.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The multiset union CMRA *)
Section gmultiset.
diff --git a/theories/algebra/gset.v b/iris/algebra/gset.v
similarity index 99%
rename from theories/algebra/gset.v
rename to iris/algebra/gset.v
index 832616e9d59c972c8ed0f055b6643e11740f2d96..c95e6c370f46309ff02b9d2d6b8b96108e39dfa3 100644
--- a/theories/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -1,7 +1,7 @@
From stdpp Require Export sets gmap mapset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates big_op.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The union CMRA *)
Section gset.
diff --git a/theories/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
similarity index 98%
rename from theories/algebra/lib/excl_auth.v
rename to iris/algebra/lib/excl_auth.v
index 307a841cc723daecc9f615611ffa9d504e752562..c410935a64f4ddcacb256f0341bcdb34be33ca86 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export auth excl updates.
From iris.algebra Require Import local_updates.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Authoritative CMRA where the fragment is exclusively owned.
This is effectively a single "ghost variable" with two views, the frament [â—¯E a]
diff --git a/theories/algebra/lib/frac_agree.v b/iris/algebra/lib/frac_agree.v
similarity index 98%
rename from theories/algebra/lib/frac_agree.v
rename to iris/algebra/lib/frac_agree.v
index af00e2bf85269b4e0ec6618aa2c8106e11a46723..6812ca9a6d717604fe5390d3126aeb0eed2374ba 100644
--- a/theories/algebra/lib/frac_agree.v
+++ b/iris/algebra/lib/frac_agree.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export frac agree updates local_updates.
From iris.algebra Require Import proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition frac_agreeR (A : ofeT) : cmraT := prodR fracR (agreeR A).
diff --git a/theories/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
similarity index 99%
rename from theories/algebra/lib/frac_auth.v
rename to iris/algebra/lib/frac_auth.v
index 6174a3e54c5c1ad608982618833e20677d57251a..b3bed379cef52bc7086a173897e993b8a29aa0b1 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export frac auth updates local_updates.
From iris.algebra Require Import proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Authoritative CMRA where the NON-authoritative parts can be fractional.
This CMRA allows the original non-authoritative element [â—¯ a] to be split into
diff --git a/theories/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
similarity index 99%
rename from theories/algebra/lib/gmap_view.v
rename to iris/algebra/lib/gmap_view.v
index 0be0eaf466ef7a25cf92a0ae2cfece9db5586c74..4c30f0144da2b6d1ca799536c0937a4505c4da19 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
From iris.algebra Require Import view updates dfrac.
From iris.algebra Require Export gmap dfrac.
From iris.algebra Require Import local_updates proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** * CMRA for a "view of a gmap".
diff --git a/theories/algebra/lib/mnat_auth.v b/iris/algebra/lib/mnat_auth.v
similarity index 98%
rename from theories/algebra/lib/mnat_auth.v
rename to iris/algebra/lib/mnat_auth.v
index aa3c062eb587d2dfd9da9c7c2c68aed0102a6273..351fa0a2f51a4bfa4cefc1a2638a5313aa1e6a75 100644
--- a/theories/algebra/lib/mnat_auth.v
+++ b/iris/algebra/lib/mnat_auth.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export auth.
From iris.algebra Require Import numbers updates.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Authoritative CMRA for [max_nat]. The authoritative element is a
monotonically increasing [nat], while a fragment is a lower bound. *)
diff --git a/theories/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
similarity index 99%
rename from theories/algebra/lib/ufrac_auth.v
rename to iris/algebra/lib/ufrac_auth.v
index 1f5705f2de9510459d5fbb908a93a2755bf8205c..e7f1f0a398799964cef7442f39b484b8314a7af2 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -18,7 +18,7 @@ difference:
*)
From iris.algebra Require Export auth frac updates local_updates.
From iris.algebra Require Import ufrac proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition ufrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR ufracR A)).
diff --git a/theories/algebra/list.v b/iris/algebra/list.v
similarity index 99%
rename from theories/algebra/list.v
rename to iris/algebra/list.v
index 798a80daa4a3b7c97f6b6208a2ec00c357498616..363a06e51b26476a0b913d79b7aee4cd5e8b0b3f 100644
--- a/theories/algebra/list.v
+++ b/iris/algebra/list.v
@@ -1,7 +1,7 @@
From stdpp Require Export list.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates big_op.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section ofe.
Context {A : ofeT}.
diff --git a/theories/algebra/local_updates.v b/iris/algebra/local_updates.v
similarity index 99%
rename from theories/algebra/local_updates.v
rename to iris/algebra/local_updates.v
index 92110f0b247e3b0148168f8ead8dc82b749816e8..c662b42293ab8a626dab6a011d285db0cd79c729 100644
--- a/theories/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** * Local updates *)
Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
diff --git a/theories/algebra/monoid.v b/iris/algebra/monoid.v
similarity index 98%
rename from theories/algebra/monoid.v
rename to iris/algebra/monoid.v
index 0c7a2e5f5b8b17ff8c58126ba2da628f9ccb8e8b..f8a563322bbab996ca801355692b9c175f17f252 100644
--- a/theories/algebra/monoid.v
+++ b/iris/algebra/monoid.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export ofe.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The Monoid class that is used for generic big operators in the file
[algebra/big_op]. The operation is an argument because we want to have multiple
diff --git a/theories/algebra/namespace_map.v b/iris/algebra/namespace_map.v
similarity index 99%
rename from theories/algebra/namespace_map.v
rename to iris/algebra/namespace_map.v
index 98656d914caea33b580950fea4813d15a710ead9..aae353ecbcea2ff2034140edeccb63f334990a27 100644
--- a/theories/algebra/namespace_map.v
+++ b/iris/algebra/namespace_map.v
@@ -1,7 +1,7 @@
From stdpp Require Import namespaces.
From iris.algebra Require Export gmap coPset local_updates.
From iris.algebra Require Import updates proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The camera [namespace_map A] over a camera [A] provides the connectives
[namespace_map_data N a], which associates data [a : A] with a namespace [N],
diff --git a/theories/algebra/numbers.v b/iris/algebra/numbers.v
similarity index 99%
rename from theories/algebra/numbers.v
rename to iris/algebra/numbers.v
index 0d73b1199e1bccf734383ade95d0e53033b76c65..fa74e117290120800db3809354260419b0ff4a10 100644
--- a/theories/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra local_updates proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** ** Natural numbers with [add] as the operation. *)
Section nat.
diff --git a/theories/algebra/ofe.v b/iris/algebra/ofe.v
similarity index 99%
rename from theories/algebra/ofe.v
rename to iris/algebra/ofe.v
index 0b0963f54a6172a35c875a23c9fb08336323d53f..135865d7e4fcadd73bb07440b7cd34494aa68930 100644
--- a/theories/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export base.
-From iris Require Import options.
+From iris.prelude Require Import options.
Set Primitive Projections.
(** This files defines (a shallow embedding of) the category of OFEs:
diff --git a/theories/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
similarity index 98%
rename from theories/algebra/proofmode_classes.v
rename to iris/algebra/proofmode_classes.v
index 7cfbdc09bc8d6b993733ff324d5aa0914810b26d..efd07f08a1b92b7893d3ee8480681729d062613f 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* There are various versions of [IsOp] with different modes:
diff --git a/theories/algebra/sts.v b/iris/algebra/sts.v
similarity index 99%
rename from theories/algebra/sts.v
rename to iris/algebra/sts.v
index fae53edbd92b431d35084883bf06c501242b3ad4..65257373f03d9a38118c3b9c0c9b94688481794a 100644
--- a/theories/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -1,7 +1,7 @@
From stdpp Require Export propset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
-From iris Require Import options.
+From iris.prelude Require Import options.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
diff --git a/theories/algebra/ufrac.v b/iris/algebra/ufrac.v
similarity index 97%
rename from theories/algebra/ufrac.v
rename to iris/algebra/ufrac.v
index 12bcf2e9f8bbf6ffaaa6fc9cc7dfc916aee1fefe..12cb7244960843a180422f07b6b215b387a6ea2f 100644
--- a/theories/algebra/ufrac.v
+++ b/iris/algebra/ufrac.v
@@ -2,7 +2,7 @@
elements are in the interval (0,..) instead of (0,1]. *)
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Since the standard (0,1] fractional camera [frac] is used more often, we
define [ufrac] through a [Definition] instead of a [Notation]. That way, Coq
diff --git a/theories/algebra/updates.v b/iris/algebra/updates.v
similarity index 99%
rename from theories/algebra/updates.v
rename to iris/algebra/updates.v
index d98af92a11b071cec7dc9ea6667493fd2c93cd50..1a671def3c9f2a3bfaf5724428e0c1250a610aeb 100644
--- a/theories/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export cmra.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** * Frame preserving updates *)
(* This quantifies over [option A] for the frame. That is necessary to
diff --git a/theories/algebra/vector.v b/iris/algebra/vector.v
similarity index 98%
rename from theories/algebra/vector.v
rename to iris/algebra/vector.v
index 17f964f61304f4d6e7d49731cab1c51e2c4de4e7..dd2a27c399ce3fe0b00c923525f69d8704ca3b7b 100644
--- a/theories/algebra/vector.v
+++ b/iris/algebra/vector.v
@@ -1,7 +1,7 @@
From stdpp Require Export vector.
From iris.algebra Require Export ofe.
From iris.algebra Require Import list.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section ofe.
Context {A : ofeT}.
diff --git a/theories/algebra/view.v b/iris/algebra/view.v
similarity index 99%
rename from theories/algebra/view.v
rename to iris/algebra/view.v
index e8ad6e623f9ed8489e1a08fb29721a8413f4eae5..3a02bf95a7b25fd600ff764d0f7a2096194d1dd4 100644
--- a/theories/algebra/view.v
+++ b/iris/algebra/view.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export updates local_updates frac agree.
From iris.algebra Require Import proofmode_classes big_op.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The view camera with fractional authoritative elements *)
(** The view camera, which is reminiscent of the views framework, is used to
diff --git a/theories/base_logic/algebra.v b/iris/base_logic/algebra.v
similarity index 99%
rename from theories/base_logic/algebra.v
rename to iris/base_logic/algebra.v
index c8d95b720b45de331dfc01ee1c6523b666b6ea05..35a40a4eec024add763b1bb83047b07f937b06d0 100644
--- a/theories/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import cmra view auth agree csum list excl gmap.
From iris.algebra.lib Require Import excl_auth gmap_view.
From iris.base_logic Require Import bi derived.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Internalized properties of our CMRA constructions. *)
diff --git a/theories/base_logic/base_logic.v b/iris/base_logic/base_logic.v
similarity index 90%
rename from theories/base_logic/base_logic.v
rename to iris/base_logic/base_logic.v
index 2c44469532d4eb17118502053e27b2b492d15131..66c98d955cdb804e0dcb8f4057c4f814a1c6af47 100644
--- a/theories/base_logic/base_logic.v
+++ b/iris/base_logic/base_logic.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi.
From iris.base_logic Require Export derived proofmode algebra.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The trick of having multiple [uPred] modules, which are all exported in
another [uPred] module is by Jason Gross and described in:
diff --git a/theories/base_logic/bi.v b/iris/base_logic/bi.v
similarity index 99%
rename from theories/base_logic/bi.v
rename to iris/base_logic/bi.v
index fa2327ae6c0df8517ad05bc054e38aaf5a0ab694..ad6814fb4cb4bc5726ac163da1d23a78d8596076 100644
--- a/theories/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -1,6 +1,6 @@
From iris.bi Require Export derived_connectives updates internal_eq plainly.
From iris.base_logic Require Export upred.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred_primitive.
(** BI instances for [uPred], and re-stating the remaining primitive laws in
diff --git a/theories/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
similarity index 99%
rename from theories/base_logic/bupd_alt.v
rename to iris/base_logic/bupd_alt.v
index 307f388509763355a70d964b891279050da82f2f..efb542d4c491f4f72b59acbc6a6d7577a988ce43 100644
--- a/theories/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export base_logic.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
Set Default Proof Using "Type*".
diff --git a/theories/base_logic/derived.v b/iris/base_logic/derived.v
similarity index 98%
rename from theories/base_logic/derived.v
rename to iris/base_logic/derived.v
index 192810f68d89c15a840b0137cd8b597bdc053c63..ad9a4c01ef4036b451e23f9651ad48e7c924f6f3 100644
--- a/theories/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import frac.
From iris.bi Require Export bi.
From iris.base_logic Require Export bi.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.bi base_logic.bi.uPred.
(** Derived laws for Iris-specific primitive connectives (own, valid).
diff --git a/theories/base_logic/lib/auth.v b/iris/base_logic/lib/auth.v
similarity index 99%
rename from theories/base_logic/lib/auth.v
rename to iris/base_logic/lib/auth.v
index 2d99ad3c102b90743203fdd22c20cde5a704038d..5733f9aa40587acd907dd6c9266ba3e935496cea 100644
--- a/theories/base_logic/lib/auth.v
+++ b/iris/base_logic/lib/auth.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(* The CMRA we need. *)
diff --git a/theories/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
similarity index 99%
rename from theories/base_logic/lib/boxes.v
rename to iris/base_logic/lib/boxes.v
index cad3771656e9710fc039b90072bdc7ca3b2c2437..8f0620e034ac5601ee4a51a20d4334e90264c1be 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import lib.excl_auth gmap agree.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(** The CMRAs we need. *)
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
similarity index 99%
rename from theories/base_logic/lib/cancelable_invariants.v
rename to iris/base_logic/lib/cancelable_invariants.v
index 0a4407c19ad0fd715cc27ec0c8ac25a26812396c..5ad576c95f142e14e165c43a0b1f94bbd9b93d6e 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export frac.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
Class cinvG Σ := cinv_inG :> inG Σ fracR.
diff --git a/theories/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
similarity index 99%
rename from theories/base_logic/lib/fancy_updates.v
rename to iris/base_logic/lib/fancy_updates.v
index 558fae055067fa77d4a9d79f4ebef5cd46022e49..7bdce06e52e41ca819bae2c76eca173aa7034da2 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import gmap auth agree gset coPset.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import wsat.
-From iris Require Import options.
+From iris.prelude Require Import options.
Export invG.
Import uPred.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/iris/base_logic/lib/fancy_updates_from_vs.v
similarity index 98%
rename from theories/base_logic/lib/fancy_updates_from_vs.v
rename to iris/base_logic/lib/fancy_updates_from_vs.v
index f1c0ccc101bbd13b47ce0240234107100cfd8ca1..a3d331e041f048674db04cac979bded9958ef859 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/iris/base_logic/lib/fancy_updates_from_vs.v
@@ -4,7 +4,7 @@ laws of the view shift. *)
From stdpp Require Export coPset.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export base_logic.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
Set Default Proof Using "Type*".
diff --git a/theories/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
similarity index 99%
rename from theories/base_logic/lib/gen_heap.v
rename to iris/base_logic/lib/gen_heap.v
index 73d9aa5a5b3570cc223e1d1ea92778bc9b2e8b67..1963deca972323d493aa4ad4e5553ecd83174172 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import gmap_view namespace_map agree frac.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(** This file provides a generic mechanism for a language-level point-to
diff --git a/theories/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
similarity index 99%
rename from theories/base_logic/lib/gen_inv_heap.v
rename to iris/base_logic/lib/gen_inv_heap.v
index b180bb9b6c587e72f572004b41f879be332849dc..da06674624ff70d661a9629958d63ca4a672fd69 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import auth excl gmap.
From iris.base_logic.lib Require Import own invariants gen_heap.
From iris.proofmode Require Import tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** An "invariant" location is a location that has some invariant about its
value attached to it, and that can never be deallocated explicitly by the
diff --git a/theories/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
similarity index 98%
rename from theories/base_logic/lib/ghost_var.v
rename to iris/base_logic/lib/ghost_var.v
index c3592a927fbf79f3d7d916371734e81abbbe6042..9c17c521a5af42ac34c2de0cca128624a8b5b6ee 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import frac_agree.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The CMRA we need. *)
Class ghost_varG Σ (A : Type) := GhostVarG {
diff --git a/theories/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
similarity index 99%
rename from theories/base_logic/lib/invariants.v
rename to iris/base_logic/lib/invariants.v
index 5fa9cd8d0d8889f74b6a5abd58f7bd744d9935c4..e7cc9b638ef0600a83cc9f7fa1fa5de407ccc083 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export fancy_updates.
From iris.base_logic.lib Require Import wsat.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(** Semantic Invariants *)
diff --git a/theories/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
similarity index 99%
rename from theories/base_logic/lib/iprop.v
rename to iris/base_logic/lib/iprop.v
index a40c6d1cf1072d3c87d58abfc50b89fc9e9a3bd3..36a4fdd4f2d470afb57ca4f7d401608121d766bb 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import gmap.
From iris.algebra Require cofe_solver.
From iris.base_logic Require Export base_logic.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** In this file we construct the type [iProp] of propositions of the Iris
logic. This is done by solving the following recursive domain equation:
diff --git a/theories/base_logic/lib/mnat.v b/iris/base_logic/lib/mnat.v
similarity index 99%
rename from theories/base_logic/lib/mnat.v
rename to iris/base_logic/lib/mnat.v
index b25f4358d47efa3f3f6bc2055cc1d26425cae1cf..b8f55488897aa2abcd1b5567f560d8a319088b87 100644
--- a/theories/base_logic/lib/mnat.v
+++ b/iris/base_logic/lib/mnat.v
@@ -12,7 +12,7 @@ From iris.algebra.lib Require Import mnat_auth.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own.
-From iris Require Import options.
+From iris.prelude Require Import options.
Class mnatG Σ :=
MnatG { mnatG_inG :> inG Σ mnat_authR; }.
diff --git a/theories/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
similarity index 99%
rename from theories/base_logic/lib/na_invariants.v
rename to iris/base_logic/lib/na_invariants.v
index 9f3f659ce232615818ac3a201166f930cc44c4a9..f4874e831937de6d0d481c872f60f3ccb3ad114c 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import gset coPset.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(* Non-atomic ("thread-local") invariants. *)
diff --git a/theories/base_logic/lib/own.v b/iris/base_logic/lib/own.v
similarity index 99%
rename from theories/base_logic/lib/own.v
rename to iris/base_logic/lib/own.v
index 3417797d88fc66204b7c03519156fefe6381a0f0..e95e32e795180d69ea7ee857e2fa1e21a2070809 100644
--- a/theories/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import functions gmap proofmode_classes.
From iris.proofmode Require Import classes.
From iris.base_logic.lib Require Export iprop.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
diff --git a/theories/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
similarity index 99%
rename from theories/base_logic/lib/proph_map.v
rename to iris/base_logic/lib/proph_map.v
index 19cacccd94283b4b1f2899fc74f64c04950cd1f2..d12feb53084a1f53ecb865b3a47d45d5c1b2cffc 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From iris.algebra Require Import gmap_view list.
From iris.base_logic.lib Require Export own.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
Local Notation proph_map P V := (gmap P (list V)).
diff --git a/theories/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
similarity index 99%
rename from theories/base_logic/lib/saved_prop.v
rename to iris/base_logic/lib/saved_prop.v
index f9915ee2b357ecfbed07c2b0b593e07408a23768..1038d4d715a73f3de79e6e7dbd337752610c42fd 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -2,7 +2,7 @@ From stdpp Require Import gmap.
From iris.algebra Require Import agree.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export own.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(* "Saved anything" -- this can give you saved propositions, saved predicates,
diff --git a/theories/base_logic/lib/sts.v b/iris/base_logic/lib/sts.v
similarity index 99%
rename from theories/base_logic/lib/sts.v
rename to iris/base_logic/lib/sts.v
index 329ead42a5efea3f83a025b1782129b8450f21b7..d4e4f8680c7144ea0492875dee49f39fe1635ffe 100644
--- a/theories/base_logic/lib/sts.v
+++ b/iris/base_logic/lib/sts.v
@@ -1,7 +1,7 @@
From iris.algebra Require Export sts.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(** The CMRA we need. *)
diff --git a/theories/base_logic/lib/viewshifts.v b/iris/base_logic/lib/viewshifts.v
similarity index 98%
rename from theories/base_logic/lib/viewshifts.v
rename to iris/base_logic/lib/viewshifts.v
index 04b3358364c02d6eeb98d2ecefb8c9c50c47944a..5aa7b55e25e1a3ea6951ff3a4db1579538e7f9d8 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/iris/base_logic/lib/viewshifts.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
□ (P -∗ |={E1,E2}=> Q).
diff --git a/theories/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
similarity index 99%
rename from theories/base_logic/lib/wsat.v
rename to iris/base_logic/lib/wsat.v
index c64dcebcdb96e2f3fcba1871562f5dad402eec01..d33c9105bb808080bd0626f4b4094978016c9bbb 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -2,7 +2,7 @@ From stdpp Require Export coPset.
From iris.algebra Require Import gmap_view gset coPset.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** All definitions in this file are internal to [fancy_updates] with the
exception of what's in the [invG] module. The module [invG] is thus exported in
diff --git a/theories/base_logic/proofmode.v b/iris/base_logic/proofmode.v
similarity index 97%
rename from theories/base_logic/proofmode.v
rename to iris/base_logic/proofmode.v
index 04d05d104117f3e38cc3341aa986e6c4fbeb5de6..dfebe074204cd4c611ce3f8b0d2dd4c06a459b9f 100644
--- a/theories/base_logic/proofmode.v
+++ b/iris/base_logic/proofmode.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import proofmode_classes.
From iris.proofmode Require Import classes.
From iris.base_logic Require Export derived.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import base_logic.bi.uPred.
diff --git a/theories/base_logic/upred.v b/iris/base_logic/upred.v
similarity index 99%
rename from theories/base_logic/upred.v
rename to iris/base_logic/upred.v
index 445ad37bad26078267ddd5c37ab0ca2e065a9068..bdb236c4e46a27b084674a053242e628666ad69f 100644
--- a/theories/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -1,7 +1,8 @@
From stdpp Require Import finite.
From iris.algebra Require Export cmra updates.
From iris.bi Require Import notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
+
Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core.
Local Hint Extern 10 (_ ≤ _) => lia : core.
diff --git a/theories/bi/ascii.v b/iris/bi/ascii.v
similarity index 99%
rename from theories/bi/ascii.v
rename to iris/bi/ascii.v
index 434592fd931fdb3b7f0fe39e0c920aedc6a6bb00..287866f6b2b62f735ed9ba62a5cc5bd6531dfd45 100644
--- a/theories/bi/ascii.v
+++ b/iris/bi/ascii.v
@@ -1,5 +1,5 @@
From iris.bi Require Import interface derived_connectives updates.
-From iris Require Import options.
+From iris.prelude Require Import options.
Notation "P |- Q" := (P ⊢ Q)
(at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
diff --git a/theories/bi/bi.v b/iris/bi/bi.v
similarity index 85%
rename from theories/bi/bi.v
rename to iris/bi/bi.v
index 66afc4ad7ea0f1b1e48c0fce76b75777b27a528e..f9ef24760a22defdb115ca31410fb57227e12191 100644
--- a/theories/bi/bi.v
+++ b/iris/bi/bi.v
@@ -1,6 +1,6 @@
From iris.bi Require Export derived_laws derived_laws_later big_op.
From iris.bi Require Export updates internal_eq plainly embedding.
-From iris Require Import options.
+From iris.prelude Require Import options.
Module Import bi.
Export bi.interface.bi.
diff --git a/theories/bi/big_op.v b/iris/bi/big_op.v
similarity index 99%
rename from theories/bi/big_op.v
rename to iris/bi/big_op.v
index 2f260da1223e33f590abb5daf2f3b52209cab694..09ac481d1b7936e153636975e3198e38c7ff9ef2 100644
--- a/theories/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2,7 +2,7 @@ From stdpp Require Import countable fin_sets functions.
From iris.algebra Require Export big_op.
From iris.algebra Require Import list gmap.
From iris.bi Require Import derived_laws_later.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(** Notations for unary variants *)
diff --git a/theories/bi/derived_connectives.v b/iris/bi/derived_connectives.v
similarity index 99%
rename from theories/bi/derived_connectives.v
rename to iris/bi/derived_connectives.v
index 671a8ae13784a2815e9ecb3691b4d968da1e18db..88e7dcca53f19f56a198e9f21662aa9da0294f45 100644
--- a/theories/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import monoid.
From iris.bi Require Export interface.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
diff --git a/theories/bi/derived_laws.v b/iris/bi/derived_laws.v
similarity index 99%
rename from theories/bi/derived_laws.v
rename to iris/bi/derived_laws.v
index aab10e497ef6f206e84b35a0bcd383c0750ae58a..8f7c63fd052680eaa36ad5d2bd4b38cb19dcda57 100644
--- a/theories/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import monoid.
From iris.bi Require Export derived_connectives.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)
Set Default Proof Using "Type*".
diff --git a/theories/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
similarity index 99%
rename from theories/bi/derived_laws_later.v
rename to iris/bi/derived_laws_later.v
index 85b375a2c6ca203b317086b07e1611312f77401e..3f61a09c42a3d8d0b9f60bf5e3ce03fd3f9caa6b 100644
--- a/theories/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import monoid.
From iris.bi Require Export derived_laws.
-From iris Require Import options.
+From iris.prelude Require Import options.
Module bi.
Import interface.bi.
diff --git a/theories/bi/embedding.v b/iris/bi/embedding.v
similarity index 99%
rename from theories/bi/embedding.v
rename to iris/bi/embedding.v
index bb73cf16aff25a4fce9395006c53d5d532f4ee2e..354028caabd165472d308e02fb54b0fd1c44b8ef 100644
--- a/theories/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import monoid.
From iris.bi Require Import interface derived_laws_later big_op.
From iris.bi Require Import plainly updates internal_eq.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
Set Default Proof Using "Type*".
diff --git a/theories/bi/interface.v b/iris/bi/interface.v
similarity index 99%
rename from theories/bi/interface.v
rename to iris/bi/interface.v
index dc7155fb2107c40fb631f7bf13524d146a542071..f3f66ba4f9fc016999aa3551268c999c779c39c4 100644
--- a/theories/bi/interface.v
+++ b/iris/bi/interface.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export ofe.
From iris.bi Require Export notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Set Primitive Projections.
Section bi_mixin.
diff --git a/theories/bi/internal_eq.v b/iris/bi/internal_eq.v
similarity index 99%
rename from theories/bi/internal_eq.v
rename to iris/bi/internal_eq.v
index df3f1a817bf9c7e06877cd697d1e0f2ff771d10a..4562e58717e7fde0d1f011612e4b108a647bbb60 100644
--- a/theories/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -1,5 +1,5 @@
From iris.bi Require Import derived_laws_later big_op.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(** This file defines a type class for BIs with a notion of internal equality.
diff --git a/theories/bi/lib/atomic.v b/iris/bi/lib/atomic.v
similarity index 99%
rename from theories/bi/lib/atomic.v
rename to iris/bi/lib/atomic.v
index d79d71a8508ad103c001ce7bf95f59c31164a694..2658652ece2efd2c39d51badde8ee80bd5c57e0b 100644
--- a/theories/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -2,7 +2,7 @@ From stdpp Require Import coPset namespaces.
From iris.bi Require Export bi updates laterable.
From iris.bi.lib Require Import fixpoint.
From iris.proofmode Require Import coq_tactics tactics reduction.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Conveniently split a conjunction on both assumption and conclusion. *)
Local Tactic Notation "iSplitWith" constr(H) :=
diff --git a/theories/bi/lib/core.v b/iris/bi/lib/core.v
similarity index 98%
rename from theories/bi/lib/core.v
rename to iris/bi/lib/core.v
index dc67214dc5e3844f94a5a6f8bcf082545f733d4b..3d2380430f8ad0ac1dab1bfa1849dd79e33e031b 100644
--- a/theories/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi plainly.
From iris.proofmode Require Import tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
(** The "core" of an assertion is its maximal persistent part,
diff --git a/theories/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
similarity index 99%
rename from theories/bi/lib/counterexamples.v
rename to iris/bi/lib/counterexamples.v
index de6465eca33d408387c6689333154f044a15c14a..23a96554fd7a4b1f5036c9c7231d5d4dff82b0c7 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi.
From iris.proofmode Require Import tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".
diff --git a/theories/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
similarity index 99%
rename from theories/bi/lib/fixpoint.v
rename to iris/bi/lib/fixpoint.v
index 8935289d8f80aaf3a634e5756d268ac029e019d8..9ca541ab8d238724d3e61a0776f9fd278a4b2a25 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi.
From iris.proofmode Require Import tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
diff --git a/theories/bi/lib/fractional.v b/iris/bi/lib/fractional.v
similarity index 99%
rename from theories/bi/lib/fractional.v
rename to iris/bi/lib/fractional.v
index 4d4b9ffa5f0661a6a677aea8257d9b4a2d2c78f5..644c47ef29330c4f3eef40004f66590acd14fca3 100644
--- a/theories/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi.
From iris.proofmode Require Import classes class_instances.
-From iris Require Import options.
+From iris.prelude Require Import options.
Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
diff --git a/theories/bi/lib/laterable.v b/iris/bi/lib/laterable.v
similarity index 99%
rename from theories/bi/lib/laterable.v
rename to iris/bi/lib/laterable.v
index eaac68789a4775ffa7c5695d86019370bd8d3915..1d11af00ca4a59e241a5f5ddc774d70bde891c9a 100644
--- a/theories/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi.
From iris.proofmode Require Import tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The class of laterable assertions *)
Class Laterable {PROP : bi} (P : PROP) := laterable :
diff --git a/theories/bi/lib/relations.v b/iris/bi/lib/relations.v
similarity index 98%
rename from theories/bi/lib/relations.v
rename to iris/bi/lib/relations.v
index 11f5d6aa75d5e2b8d3b825d103691d909d7792e9..1d1d09ffea98017be3b11e2da4814f33b342b381 100644
--- a/theories/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -2,7 +2,7 @@
its reflexive transitive closure. *)
From iris.bi.lib Require Export fixpoint.
From iris.proofmode Require Import tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".
diff --git a/theories/bi/monpred.v b/iris/bi/monpred.v
similarity index 99%
rename from theories/bi/monpred.v
rename to iris/bi/monpred.v
index f2bb21e9a3f0d255a31d0ab44790c21675dbce3d..d1f047eb42a687c9efd9993f29453a18c3c3734c 100644
--- a/theories/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -1,6 +1,6 @@
From stdpp Require Import coPset.
From iris.bi Require Import bi.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Definitions. *)
Structure biIndex :=
diff --git a/theories/bi/notation.v b/iris/bi/notation.v
similarity index 99%
rename from theories/bi/notation.v
rename to iris/bi/notation.v
index bea7f6b417b49412d3a49eb7e09defa70a4af5cf..117ced195b6f84951193b3027df77d98975e2d36 100644
--- a/theories/bi/notation.v
+++ b/iris/bi/notation.v
@@ -1,4 +1,4 @@
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Just reserve the notation. *)
(** * Turnstiles *)
diff --git a/theories/bi/plainly.v b/iris/bi/plainly.v
similarity index 99%
rename from theories/bi/plainly.v
rename to iris/bi/plainly.v
index c35d743797a539320a0d0e3390a20c1ee8786678..4d2439693a914b185a7799e0d7eb1bc522b72220 100644
--- a/theories/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import monoid.
From iris.bi Require Import derived_laws_later big_op internal_eq.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
diff --git a/theories/bi/telescopes.v b/iris/bi/telescopes.v
similarity index 98%
rename from theories/bi/telescopes.v
rename to iris/bi/telescopes.v
index 2bef8b0e78e131b20140a3b57642ac86d031419f..b2836192c84f085f32e677d9d9c64b8ce24a9d03 100644
--- a/theories/bi/telescopes.v
+++ b/iris/bi/telescopes.v
@@ -1,6 +1,6 @@
From stdpp Require Export telescopes.
From iris.bi Require Export bi.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
(* This cannot import the proofmode because it is imported by the proofmode! *)
diff --git a/theories/bi/updates.v b/iris/bi/updates.v
similarity index 99%
rename from theories/bi/updates.v
rename to iris/bi/updates.v
index 0674386abc4d2714d604fbd9c6128a51d077baf9..65b06d2514aefb11ca3637ec0a40c9bd17111239 100644
--- a/theories/bi/updates.v
+++ b/iris/bi/updates.v
@@ -1,6 +1,6 @@
From stdpp Require Import coPset.
From iris.bi Require Import interface derived_laws_later big_op plainly.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
diff --git a/theories/bi/weakestpre.v b/iris/bi/weakestpre.v
similarity index 99%
rename from theories/bi/weakestpre.v
rename to iris/bi/weakestpre.v
index ee7181d5cdefbe4c500410a268f0e7a31a0c1760..75963fa02e3b407c9c0864c02b89d1b6febf3a98 100644
--- a/theories/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -1,7 +1,7 @@
From stdpp Require Export coPset.
From iris.bi Require Import interface derived_connectives.
From iris.program_logic Require Import language.
-From iris Require Import options.
+From iris.prelude Require Import options.
Inductive stuckness := NotStuck | MaybeStuck.
diff --git a/theories/options.v b/iris/prelude/options.v
similarity index 93%
rename from theories/options.v
rename to iris/prelude/options.v
index 1e4c1f31180de56458fb5f0c68d15a150293786e..22d74e4a485069bc1cc8ce71dcf386d6e840b23a 100644
--- a/theories/options.v
+++ b/iris/prelude/options.v
@@ -12,5 +12,5 @@ Export Set Default Goal Selector "!".
(* "Fake" import to whitelist this file for the check that ensures we import
this file everywhere.
-From iris Require Import options.
+From iris.prelude Require Import options.
*)
diff --git a/theories/program_logic/adequacy.v b/iris/program_logic/adequacy.v
similarity index 99%
rename from theories/program_logic/adequacy.v
rename to iris/program_logic/adequacy.v
index 612af7f2996ec4101ee3209c06c81e4f18be33f0..ef2abff218b916020e2fb5dd7de661babd2feb06 100644
--- a/theories/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import gmap auth agree gset coPset.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import wsat.
From iris.program_logic Require Export weakestpre.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(** This file contains the adequacy statements of the Iris program logic. First
diff --git a/theories/program_logic/atomic.v b/iris/program_logic/atomic.v
similarity index 99%
rename from theories/program_logic/atomic.v
rename to iris/program_logic/atomic.v
index 13be0ce35f1feccebdedc00a519b03f293f3dfa1..04a07d03ef49c36280da23a82ed4f7c72a028d7a 100644
--- a/theories/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -4,7 +4,7 @@ From iris.bi.lib Require Export atomic.
From iris.proofmode Require Import tactics classes.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import invariants.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* This hard-codes the inner mask to be empty, because we have yet to find an
example where we want it to be anything else. *)
diff --git a/theories/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
similarity index 99%
rename from theories/program_logic/ectx_language.v
rename to iris/program_logic/ectx_language.v
index ebf94a86747033358269852e0dcf7fed32816f05..a76f590edcf6cff23fa1f8fba2289b525ca8f81f 100644
--- a/theories/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -2,7 +2,7 @@
that this gives rise to a "language" in the Iris sense. *)
From iris.algebra Require Export base.
From iris.program_logic Require Import language.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** TAKE CARE: When you define an [ectxLanguage] canonical structure for your
language, you need to also define a corresponding [language] canonical
diff --git a/theories/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
similarity index 99%
rename from theories/program_logic/ectx_lifting.v
rename to iris/program_logic/ectx_lifting.v
index 926ae75c554eb27f2e558bde25d825ee3bf28608..11372d1c7750545bf738f4381d06dce5be7713e7 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -1,7 +1,7 @@
(** Some derived lemmas for ectx-based languages *)
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export ectx_language weakestpre lifting.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section wp.
Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
diff --git a/theories/program_logic/ectxi_language.v b/iris/program_logic/ectxi_language.v
similarity index 99%
rename from theories/program_logic/ectxi_language.v
rename to iris/program_logic/ectxi_language.v
index e9e9477c5f5a7a61ff9b1b534c87a3b936fa9058..e3a245b2e4912303db0bed39c08ef405452a9878 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/iris/program_logic/ectxi_language.v
@@ -2,7 +2,7 @@
a proof that these are instances of general ectx-based languages. *)
From iris.algebra Require Export base.
From iris.program_logic Require Import language ectx_language.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** TAKE CARE: When you define an [ectxiLanguage] canonical structure for your
language, you need to also define a corresponding [language] and [ectxLanguage]
diff --git a/theories/program_logic/hoare.v b/iris/program_logic/hoare.v
similarity index 99%
rename from theories/program_logic/hoare.v
rename to iris/program_logic/hoare.v
index b08d144fbf58be19cb1f5b1fc59932d77ba06fe3..45f9702cda33308c10701ed9f6ce8411141801a5 100644
--- a/theories/program_logic/hoare.v
+++ b/iris/program_logic/hoare.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export viewshifts.
From iris.program_logic Require Export weakestpre.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
(e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/theories/program_logic/language.v b/iris/program_logic/language.v
similarity index 99%
rename from theories/program_logic/language.v
rename to iris/program_logic/language.v
index 603391006be668ebc30a8b6e1223414199da8f10..c599f97c93ea499bb182593cad42ef426fe65913 100644
--- a/theories/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export ofe.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section language_mixin.
Context {expr val state observation : Type}.
diff --git a/theories/program_logic/lifting.v b/iris/program_logic/lifting.v
similarity index 99%
rename from theories/program_logic/lifting.v
rename to iris/program_logic/lifting.v
index bb5fa43d662c2d450ab3c0edfbef4498ff35574e..9b532e703650ff8286a6d1c2082d79f7a3006ae3 100644
--- a/theories/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -3,7 +3,7 @@ semantics to the program logic. *)
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section lifting.
Context `{!irisG Λ Σ}.
diff --git a/theories/program_logic/ownp.v b/iris/program_logic/ownp.v
similarity index 99%
rename from theories/program_logic/ownp.v
rename to iris/program_logic/ownp.v
index 78e6ffcf9bdc044edb08677675c277bf42f4fc3f..9b8e438be1a5e1f2bcb549a5366ed79bc8da59e3 100644
--- a/theories/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics classes.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
-From iris Require Import options.
+From iris.prelude Require Import options.
(**
This module provides an interface to handling ownership of the global state that
diff --git a/theories/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
similarity index 99%
rename from theories/program_logic/total_adequacy.v
rename to iris/program_logic/total_adequacy.v
index 1825b3cd9779245e1de2c2f0e3c3c590c4b1998e..19ffe2810756a8e749fecc599089ddc6d8eeafb3 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import gmap auth agree gset coPset list.
From iris.bi Require Import big_op fixpoint.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export total_weakestpre adequacy.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
Section adequacy.
diff --git a/theories/program_logic/total_ectx_lifting.v b/iris/program_logic/total_ectx_lifting.v
similarity index 98%
rename from theories/program_logic/total_ectx_lifting.v
rename to iris/program_logic/total_ectx_lifting.v
index 99c34b6d3b85db35fff72f208b3aa6046af791f2..2d0d1043db9ecb81b232e7cee3fbf3e56277aa9c 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/iris/program_logic/total_ectx_lifting.v
@@ -1,7 +1,7 @@
(** Some derived lemmas for ectx-based languages *)
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export ectx_language total_weakestpre total_lifting.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section wp.
Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
diff --git a/theories/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
similarity index 98%
rename from theories/program_logic/total_lifting.v
rename to iris/program_logic/total_lifting.v
index 19b9af5a28a72f19f3234397d44ab6adf2b952c4..c1e4eb617859d4f803e99ecda46b97f82a276233 100644
--- a/theories/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -1,7 +1,7 @@
From iris.bi Require Export big_op.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export total_weakestpre.
-From iris Require Import options.
+From iris.prelude Require Import options.
Section lifting.
Context `{!irisG Λ Σ}.
diff --git a/theories/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
similarity index 99%
rename from theories/program_logic/total_weakestpre.v
rename to iris/program_logic/total_weakestpre.v
index 1fa5c032451c0deda1c75b38eb8a6a57143415e2..e1aa91555d668bf9a8203af1bf5861bca5206474 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -1,7 +1,7 @@
From iris.bi Require Import fixpoint big_op.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
(** The definition of total weakest preconditions is very similar to the
diff --git a/theories/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
similarity index 99%
rename from theories/program_logic/weakestpre.v
rename to iris/program_logic/weakestpre.v
index e0d639fb6695e7c444be1b52e18ac02f97c323b8..a80ee8512f2bf454398fb19b54f2e1203365e9a9 100644
--- a/theories/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export language.
(* FIXME: If we import iris.bi.weakestpre earlier texan triples do not
get pretty-printed correctly. *)
From iris.bi Require Export weakestpre.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
diff --git a/theories/proofmode/base.v b/iris/proofmode/base.v
similarity index 98%
rename from theories/proofmode/base.v
rename to iris/proofmode/base.v
index abf4e1361f3018b81cf72a25d2a288f61c5a1a23..5a969fea020a852e90c570fc14d6705255698481 100644
--- a/theories/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -1,7 +1,7 @@
From Coq Require Export Ascii.
From stdpp Require Export strings.
From iris.algebra Require Export base.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** * Utility definitions used by the proofmode *)
diff --git a/theories/proofmode/class_instances.v b/iris/proofmode/class_instances.v
similarity index 99%
rename from theories/proofmode/class_instances.v
rename to iris/proofmode/class_instances.v
index 502326653c7672a06f2219b79cf99bfbb91bba18..8b5f315fbffb79d0bcb632ee3e7133b97406065c 100644
--- a/theories/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -2,7 +2,7 @@ From stdpp Require Import nat_cancel.
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import base modality_instances classes.
From iris.proofmode Require Import ltac_tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
(* FIXME(Coq #6294): needs new unification *)
diff --git a/theories/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v
similarity index 99%
rename from theories/proofmode/class_instances_embedding.v
rename to iris/proofmode/class_instances_embedding.v
index c75f275345fa173a6eadf31178ac849ec2179c89..e355153ea361e7aab078879ab328390a35218201 100644
--- a/theories/proofmode/class_instances_embedding.v
+++ b/iris/proofmode/class_instances_embedding.v
@@ -1,6 +1,6 @@
From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
(** We add a useless hypothesis [BiEmbed PROP PROP'] in order to make sure this
diff --git a/theories/proofmode/class_instances_internal_eq.v b/iris/proofmode/class_instances_internal_eq.v
similarity index 98%
rename from theories/proofmode/class_instances_internal_eq.v
rename to iris/proofmode/class_instances_internal_eq.v
index c75ead317fd516cc433597c003cc86ee774ba5e4..a8cf210e73777010b3b723b6abfcc798e1fbd089 100644
--- a/theories/proofmode/class_instances_internal_eq.v
+++ b/iris/proofmode/class_instances_internal_eq.v
@@ -1,7 +1,7 @@
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Section class_instances_internal_eq.
diff --git a/theories/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
similarity index 99%
rename from theories/proofmode/class_instances_later.v
rename to iris/proofmode/class_instances_later.v
index ffab7068c7775a9012011705441a422f8b652f5c..d4c7e2d3ab7c29bdab0946e2b340a679bfdbf776 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -1,7 +1,7 @@
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Section class_instances_later.
diff --git a/theories/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
similarity index 99%
rename from theories/proofmode/class_instances_plainly.v
rename to iris/proofmode/class_instances_plainly.v
index f3eba370e60e2c96f850a1b3bda79af5454bc51f..b49f42a76c3a2ac3d24ca5a53c147eef3cccd943 100644
--- a/theories/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -1,6 +1,6 @@
From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Section class_instances_plainly.
diff --git a/theories/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
similarity index 99%
rename from theories/proofmode/class_instances_updates.v
rename to iris/proofmode/class_instances_updates.v
index 9bc9f38aa36b7772b16d121c721bbe02e328a089..0e0a116d5fa08d7dad97919d44201df2dda12390 100644
--- a/theories/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -2,7 +2,7 @@ From stdpp Require Import nat_cancel.
From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
From iris.proofmode Require Import ltac_tactics class_instances.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Section class_instances_updates.
diff --git a/theories/proofmode/classes.v b/iris/proofmode/classes.v
similarity index 99%
rename from theories/proofmode/classes.v
rename to iris/proofmode/classes.v
index 9c1d7af95e05a9d120ed2ca5facdee8b2c6dbb2a..b71455cd7e8605a794b309a902db41a99f9e10c6 100644
--- a/theories/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -2,7 +2,7 @@ From stdpp Require Import namespaces.
From iris.bi Require Export bi.
From iris.proofmode Require Import base.
From iris.proofmode Require Export ident_name modalities.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
diff --git a/theories/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
similarity index 99%
rename from theories/proofmode/coq_tactics.v
rename to iris/proofmode/coq_tactics.v
index 3987d63bc92de67854812fad90236c13a031103f..5aee11b50a4af7d5b3b11cb778ac7388e73dd8ad 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi telescopes.
From iris.proofmode Require Export base environments classes modality_instances.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Import env_notations.
diff --git a/theories/proofmode/environments.v b/iris/proofmode/environments.v
similarity index 99%
rename from theories/proofmode/environments.v
rename to iris/proofmode/environments.v
index e77b6b44eff752ee9062629c38aed7470aa7e9ff..e185690dc538dc25a5d149fe0731876c52d169d2 100644
--- a/theories/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -1,7 +1,7 @@
From iris.algebra Require Export base.
From iris.bi Require Export bi.
From iris.proofmode Require Import base.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Inductive env (A : Type) : Type :=
diff --git a/theories/proofmode/frame_instances.v b/iris/proofmode/frame_instances.v
similarity index 99%
rename from theories/proofmode/frame_instances.v
rename to iris/proofmode/frame_instances.v
index 11c96ddcc689c2bb5598e96087d1cabd974fb16c..291e326b71f7171665b8a6ba309f19c83fcabc58 100644
--- a/theories/proofmode/frame_instances.v
+++ b/iris/proofmode/frame_instances.v
@@ -1,7 +1,7 @@
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
(** This file defines the instances that make up the framing machinery. *)
diff --git a/theories/proofmode/ident_name.v b/iris/proofmode/ident_name.v
similarity index 97%
rename from theories/proofmode/ident_name.v
rename to iris/proofmode/ident_name.v
index 136493f1305ab4de09300b0d561ebd2035e47f9c..709205e3e2082d41de2c355dd40d9fcb71710019 100644
--- a/theories/proofmode/ident_name.v
+++ b/iris/proofmode/ident_name.v
@@ -1,5 +1,5 @@
From stdpp Require Import base.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** [ident_name] is a way to remember an identifier within the binder of a
(trivial) function, which can be constructed and retrieved with Ltac but is easy
diff --git a/theories/proofmode/intro_patterns.v b/iris/proofmode/intro_patterns.v
similarity index 99%
rename from theories/proofmode/intro_patterns.v
rename to iris/proofmode/intro_patterns.v
index d5895ebdcfa6c267dbb18d9dadf0b436aab46bad..4847e2aca14d192056a36eaa6c9e7090ec6120b6 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/iris/proofmode/intro_patterns.v
@@ -1,6 +1,6 @@
From stdpp Require Export strings.
From iris.proofmode Require Import base tokens sel_patterns.
-From iris Require Import options.
+From iris.prelude Require Import options.
Inductive gallina_ident :=
| IGallinaNamed : string → gallina_ident
diff --git a/theories/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
similarity index 99%
rename from theories/proofmode/ltac_tactics.v
rename to iris/proofmode/ltac_tactics.v
index 6cd5e2e4c6b9f187281eab5151656f8997ce54ba..5cb16a875a70da6928a5aa79c89412ce073f498f 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3,7 +3,7 @@ From iris.bi Require Export bi telescopes.
From iris.proofmode Require Import base intro_patterns spec_patterns
sel_patterns coq_tactics reduction.
From iris.proofmode Require Export classes notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Export ident.
(** For most of the tactics, we want to have tight control over the order and
diff --git a/theories/proofmode/modalities.v b/iris/proofmode/modalities.v
similarity index 99%
rename from theories/proofmode/modalities.v
rename to iris/proofmode/modalities.v
index cc33f63bd1c3a5f3712a78d5142400c20f2da66c..1e65317da69d07e0b76f6623903d0475bfa6e589 100644
--- a/theories/proofmode/modalities.v
+++ b/iris/proofmode/modalities.v
@@ -1,6 +1,6 @@
From stdpp Require Import namespaces.
From iris.bi Require Export bi.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
(** The `iModIntro` tactic is not tied the Iris modalities, but can be
diff --git a/theories/proofmode/modality_instances.v b/iris/proofmode/modality_instances.v
similarity index 98%
rename from theories/proofmode/modality_instances.v
rename to iris/proofmode/modality_instances.v
index 23d93c65e33cbbd392e48304fafa74359270e381..ea0d67984b7965c661132a95d3a443aef8d3dc72 100644
--- a/theories/proofmode/modality_instances.v
+++ b/iris/proofmode/modality_instances.v
@@ -1,6 +1,6 @@
From iris.bi Require Import bi.
From iris.proofmode Require Export classes.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import bi.
Section modalities.
diff --git a/theories/proofmode/monpred.v b/iris/proofmode/monpred.v
similarity index 99%
rename from theories/proofmode/monpred.v
rename to iris/proofmode/monpred.v
index e9012f26876348a470bc834fde5e439fa9534d96..f59f09245a46da1b9618fd3d39cf9e93765e7134 100644
--- a/theories/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -1,7 +1,7 @@
From iris.bi Require Export monpred.
From iris.bi Require Import plainly.
From iris.proofmode Require Import tactics modality_instances.
-From iris Require Import options.
+From iris.prelude Require Import options.
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
(P : monPred I PROP) (ð“Ÿ : PROP) :=
diff --git a/theories/proofmode/notation.v b/iris/proofmode/notation.v
similarity index 97%
rename from theories/proofmode/notation.v
rename to iris/proofmode/notation.v
index d2812ef7a44f24bf2ded5eb1a0ab87bce1c48fef..0f4fd26c0b8a1816f68921a4ea9c21519593959d 100644
--- a/theories/proofmode/notation.v
+++ b/iris/proofmode/notation.v
@@ -1,6 +1,6 @@
From stdpp Require Export strings.
From iris.proofmode Require Import coq_tactics environments.
-From iris Require Import options.
+From iris.prelude Require Import options.
Declare Scope proof_scope.
Delimit Scope proof_scope with env.
diff --git a/theories/proofmode/reduction.v b/iris/proofmode/reduction.v
similarity index 97%
rename from theories/proofmode/reduction.v
rename to iris/proofmode/reduction.v
index c92ba206bd0ccaa7e8cf5201d298bc2a595931b4..b70aef0a39f3fb4edde630b0d2657e13902ca3ba 100644
--- a/theories/proofmode/reduction.v
+++ b/iris/proofmode/reduction.v
@@ -1,6 +1,6 @@
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import base environments.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Called by all tactics to perform computation to lookup items in the
context. We avoid reducing anything user-visible here to make sure we
diff --git a/theories/proofmode/sel_patterns.v b/iris/proofmode/sel_patterns.v
similarity index 96%
rename from theories/proofmode/sel_patterns.v
rename to iris/proofmode/sel_patterns.v
index 0b360c19647ea0f0e05004d9d5bfa6c293a2285d..6f498a36560fd998624152ebf123f497ff1bdfa2 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/iris/proofmode/sel_patterns.v
@@ -1,6 +1,6 @@
From stdpp Require Export strings.
From iris.proofmode Require Import base tokens.
-From iris Require Import options.
+From iris.prelude Require Import options.
Inductive sel_pat :=
| SelPure
diff --git a/theories/proofmode/spec_patterns.v b/iris/proofmode/spec_patterns.v
similarity index 98%
rename from theories/proofmode/spec_patterns.v
rename to iris/proofmode/spec_patterns.v
index b2edc3b4c8181b4e7cf91479c559193b3254abb7..983b6d260479db08838c0de29ca30e22ba54b9df 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/iris/proofmode/spec_patterns.v
@@ -1,6 +1,6 @@
From stdpp Require Export strings.
From iris.proofmode Require Import base tokens.
-From iris Require Import options.
+From iris.prelude Require Import options.
Inductive goal_kind := GSpatial | GModal | GIntuitionistic.
diff --git a/theories/proofmode/tactics.v b/iris/proofmode/tactics.v
similarity index 90%
rename from theories/proofmode/tactics.v
rename to iris/proofmode/tactics.v
index 6fdca9b1e416ceb7bdb9f55fb2c72185b6675cda..f7680f074e4b30ff099cf9ab1235c10dcd2d3c51 100644
--- a/theories/proofmode/tactics.v
+++ b/iris/proofmode/tactics.v
@@ -5,4 +5,4 @@ From iris.proofmode Require Import class_instances class_instances_later
class_instances_updates class_instances_embedding
class_instances_plainly class_instances_internal_eq.
From iris.proofmode Require Import frame_instances modality_instances.
-From iris Require Import options.
+From iris.prelude Require Import options.
diff --git a/theories/proofmode/tokens.v b/iris/proofmode/tokens.v
similarity index 98%
rename from theories/proofmode/tokens.v
rename to iris/proofmode/tokens.v
index b7d075007d0f8b129785f27750eb11af79bcd1f2..a450d6c2fea4d9c4959174ab547df052370fad5b 100644
--- a/theories/proofmode/tokens.v
+++ b/iris/proofmode/tokens.v
@@ -1,5 +1,5 @@
From iris.proofmode Require Import base.
-From iris Require Import options.
+From iris.prelude Require Import options.
Inductive token :=
| TName : string → token
diff --git a/theories/si_logic/bi.v b/iris/si_logic/bi.v
similarity index 99%
rename from theories/si_logic/bi.v
rename to iris/si_logic/bi.v
index 6dbcd41a34c1c9529af05f1d7c3b3846c46e2490..dc8be0254f5409df314fbe055b779af1ca3c18f5 100644
--- a/theories/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi.
From iris.si_logic Require Export siprop.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import siProp_primitive.
(** BI instances for [siProp], and re-stating the remaining primitive laws in
diff --git a/theories/si_logic/siprop.v b/iris/si_logic/siprop.v
similarity index 99%
rename from theories/si_logic/siprop.v
rename to iris/si_logic/siprop.v
index 30343ff494346216306dfd3917d5e3768d14f97d..345994a211c472d5b5643c68c0ccca3d8b4879bd 100644
--- a/theories/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -1,6 +1,6 @@
From iris.algebra Require Export ofe.
From iris.bi Require Import notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The type [siProp] defines "plain" step-indexed propositions, on which we
define the usual connectives of higher-order logic, and prove that these satisfy
diff --git a/theories/heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
similarity index 96%
rename from theories/heap_lang/adequacy.v
rename to iris_heap_lang/adequacy.v
index ed24c8ae31e48f1d1cb52651002b124ea9837a15..a1d218d3d91f0edc36bea6a5f6edc052dc116481 100644
--- a/theories/heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import auth.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
diff --git a/theories/heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
similarity index 99%
rename from theories/heap_lang/derived_laws.v
rename to iris_heap_lang/derived_laws.v
index 4a394f6b61070c69a0f76ba688108bce23634226..addf300bad70e2ce2290ef2449e2956b792fe269 100644
--- a/theories/heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -9,7 +9,7 @@ From iris.bi Require Import lib.fractional.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export primitive_laws.
From iris.heap_lang Require Import tactics notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The [array] connective is a version of [mapsto] that works
with lists of values. *)
diff --git a/theories/heap_lang/lang.v b/iris_heap_lang/lang.v
similarity index 99%
rename from theories/heap_lang/lang.v
rename to iris_heap_lang/lang.v
index 7d4f4f0b53a600fa18ceb84c43655982e23a9da6..226b4e183ce1985c7ca20207036bdb5095e89bbc 100644
--- a/theories/heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -3,7 +3,7 @@ From stdpp Require Import gmap.
From iris.algebra Require Export ofe.
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.heap_lang Require Export locations.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** heap_lang. A fairly simple language used for common Iris examples.
diff --git a/theories/heap_lang/lib/arith.v b/iris_heap_lang/lib/arith.v
similarity index 97%
rename from theories/heap_lang/lib/arith.v
rename to iris_heap_lang/lib/arith.v
index 501cfbabc553961293159f97b3f09c584ac61d68..8a2165ce6becbac4b2e21575bfa4ef66d3abcd62 100644
--- a/theories/heap_lang/lib/arith.v
+++ b/iris_heap_lang/lib/arith.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** A library defining binary [minimum] and [maximum] functions, together with
their expected specs. These operations come up often when working manipulating
diff --git a/theories/heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
similarity index 99%
rename from theories/heap_lang/lib/array.v
rename to iris_heap_lang/lib/array.v
index f7e2bd7bd9c082739d4290c6c2063e1118782ce7..40f8387df0c82536d53deb2401e276caad9c7d63 100644
--- a/theories/heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export derived_laws.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Provides some array utilities:
diff --git a/theories/heap_lang/lib/assert.v b/iris_heap_lang/lib/assert.v
similarity index 95%
rename from theories/heap_lang/lib/assert.v
rename to iris_heap_lang/lib/assert.v
index db8adb8d66004abb466db5c50c685babc34c13e3..1397a3380b8fdd0c53c76a44ddaf63f2cfc8ed87 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/iris_heap_lang/lib/assert.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
diff --git a/theories/heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
similarity index 99%
rename from theories/heap_lang/lib/atomic_heap.v
rename to iris_heap_lang/lib/atomic_heap.v
index f39fc9d07de43e278ffecb761c0b28b8955b321d..0679e493f1fee8ea436cf78da9558db95e85fe8f 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export derived_laws.
From iris.heap_lang Require Import notation proofmode.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** A general logically atomic interface for a heap. *)
Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
diff --git a/theories/heap_lang/lib/clairvoyant_coin.v b/iris_heap_lang/lib/clairvoyant_coin.v
similarity index 98%
rename from theories/heap_lang/lib/clairvoyant_coin.v
rename to iris_heap_lang/lib/clairvoyant_coin.v
index 70673ad50872c46a134b9ae74d333e8cefcce568..e840732bbfcb50fa08eda7d641f65d85af76a940 100644
--- a/theories/heap_lang/lib/clairvoyant_coin.v
+++ b/iris_heap_lang/lib/clairvoyant_coin.v
@@ -2,7 +2,7 @@ From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** The clairvoyant coin predicts all the values that it will
*non-deterministically* choose throughout the execution of the
diff --git a/theories/heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
similarity index 99%
rename from theories/heap_lang/lib/counter.v
rename to iris_heap_lang/lib/counter.v
index 48537d024b8dd3b26a95d3055bcb2bcbc61d8308..378b03fcf0552dff46e9d612e154903fd7ec48c9 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" :=
diff --git a/theories/heap_lang/lib/diverge.v b/iris_heap_lang/lib/diverge.v
similarity index 96%
rename from theories/heap_lang/lib/diverge.v
rename to iris_heap_lang/lib/diverge.v
index 393445f46dc820636a3aaaa8d761e18de35dcdca..18a27c2f2cd7bf135804e6d313e901f24c00623e 100644
--- a/theories/heap_lang/lib/diverge.v
+++ b/iris_heap_lang/lib/diverge.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** This library provides a [diverge] function that goes into an infinite loop
when provided with an (arbitrary) argument value. This function can be used to
diff --git a/theories/heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
similarity index 99%
rename from theories/heap_lang/lib/increment.v
rename to iris_heap_lang/lib/increment.v
index bf71e6f3b72336af0834728ee6c88ae3ac2d966a..604ecac1bb2543ff22b08b45fe4e3fc80e9249e4 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation atomic_heap par.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Show that implementing fetch-and-add on top of CAS preserves logical
atomicity. *)
diff --git a/theories/heap_lang/lib/lazy_coin.v b/iris_heap_lang/lib/lazy_coin.v
similarity index 97%
rename from theories/heap_lang/lib/lazy_coin.v
rename to iris_heap_lang/lib/lazy_coin.v
index 315cc5f3f88f28ee9030e6db500407934d690b42..588380e97c42dac16a12d085b897a179ff44d242 100644
--- a/theories/heap_lang/lib/lazy_coin.v
+++ b/iris_heap_lang/lib/lazy_coin.v
@@ -2,7 +2,7 @@ From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition new_coin: val := λ: <>, (ref NONE, NewProph).
diff --git a/theories/heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
similarity index 97%
rename from theories/heap_lang/lib/lock.v
rename to iris_heap_lang/lib/lock.v
index 8edd581e41b0f4ea071e6b026be64b4c116c3ee4..c34a7736899cc0a3ba85f2d3a06d4b18fdb55dfb 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -1,6 +1,6 @@
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Import primitive_laws notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Structure lock Σ `{!heapG Σ} := Lock {
(** * Operations *)
diff --git a/theories/heap_lang/lib/nondet_bool.v b/iris_heap_lang/lib/nondet_bool.v
similarity index 94%
rename from theories/heap_lang/lib/nondet_bool.v
rename to iris_heap_lang/lib/nondet_bool.v
index 98aec67e0dd8f8ffad59782dca8f547316de6589..f81d48ccebbe3e877eb3fa33f4336586fd5556f2 100644
--- a/theories/heap_lang/lib/nondet_bool.v
+++ b/iris_heap_lang/lib/nondet_bool.v
@@ -1,7 +1,7 @@
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition nondet_bool : val :=
λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".
diff --git a/theories/heap_lang/lib/par.v b/iris_heap_lang/lib/par.v
similarity index 97%
rename from theories/heap_lang/lib/par.v
rename to iris_heap_lang/lib/par.v
index fb33eb8003808a792c6c09a7974c16d040bc9a69..ad40461004a8d3050db35a43eddf937c261b8684 100644
--- a/theories/heap_lang/lib/par.v
+++ b/iris_heap_lang/lib/par.v
@@ -1,6 +1,6 @@
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Export spawn.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
Definition parN : namespace := nroot .@ "par".
diff --git a/theories/heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
similarity index 98%
rename from theories/heap_lang/lib/spawn.v
rename to iris_heap_lang/lib/spawn.v
index 0d033c5d1079ea5b8e266f27d3b965c54b916afc..8be6983d54146c1538c272ef277f5d1f8791755b 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition spawn : val :=
λ: "f",
diff --git a/theories/heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
similarity index 99%
rename from theories/heap_lang/lib/spin_lock.v
rename to iris_heap_lang/lib/spin_lock.v
index 8f4986496c807a4cd75a824dd95079590a0f2079..a847b985a51807641c25957b52b0b357e3ceae11 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import lock.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
similarity index 99%
rename from theories/heap_lang/lib/ticket_lock.v
rename to iris_heap_lang/lib/ticket_lock.v
index 5b202eaed32f998c5b48d80cf83e6d491486c7cc..55856b30467f3adc3694787e031d81c5a31e306f 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Export lock.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition wait_loop: val :=
rec: "wait_loop" "x" "lk" :=
diff --git a/theories/heap_lang/locations.v b/iris_heap_lang/locations.v
similarity index 97%
rename from theories/heap_lang/locations.v
rename to iris_heap_lang/locations.v
index 146b3816aca6f39d7b4b56f5909e9c5d6b8a3041..7cca50788928e1b14fead5d0599d624751d8e762 100644
--- a/theories/heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -1,6 +1,6 @@
From stdpp Require Import countable numbers gmap.
From iris.algebra Require Import base.
-From iris Require Import options.
+From iris.prelude Require Import options.
Record loc := { loc_car : Z }.
diff --git a/theories/heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
similarity index 99%
rename from theories/heap_lang/metatheory.v
rename to iris_heap_lang/metatheory.v
index 106a1242398fde8492313962bbae567fc9e56cb8..54619aa4ab41e61826153a9089e78797fa18dd19 100644
--- a/theories/heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -1,6 +1,6 @@
From stdpp Require Import gmap.
From iris.heap_lang Require Export lang.
-From iris Require Import options.
+From iris.prelude Require Import options.
(* This file contains some metatheory about the heap_lang language,
which is not needed for verifying programs. *)
diff --git a/theories/heap_lang/notation.v b/iris_heap_lang/notation.v
similarity index 99%
rename from theories/heap_lang/notation.v
rename to iris_heap_lang/notation.v
index f9948af37616d34af23209e3c10426d537324c3b..6ea7e8eaab90a9a81d1d5ca063b227d732ceafbf 100644
--- a/theories/heap_lang/notation.v
+++ b/iris_heap_lang/notation.v
@@ -1,6 +1,6 @@
From iris.program_logic Require Import language.
From iris.heap_lang Require Export lang.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** Coercions to make programs easier to type. *)
Coercion LitInt : Z >-> base_lit.
diff --git a/theories/heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
similarity index 99%
rename from theories/heap_lang/primitive_laws.v
rename to iris_heap_lang/primitive_laws.v
index ce297d8e6eeca46222ac65b49b069b2d8b2f9b2a..36deec1e87495d631f0525283e756acff936e750 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -10,7 +10,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
diff --git a/theories/heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
similarity index 99%
rename from theories/heap_lang/proofmode.v
rename to iris_heap_lang/proofmode.v
index 6eaf109e165a6c201af66b34e84a8a945c963222..8826570fa48047f6ec29d893c13bcba692daa9f1 100644
--- a/theories/heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Export tactics.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Export tactics derived_laws.
From iris.heap_lang Require Import notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import uPred.
Lemma tac_wp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
diff --git a/theories/heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
similarity index 99%
rename from theories/heap_lang/proph_erasure.v
rename to iris_heap_lang/proph_erasure.v
index 4cfeef1bc4497d9e00bedd0bb33f58f5c842ce87..750b55bd4a852230ce59d89eb47a2c8fe6cfc6da 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -1,6 +1,6 @@
From iris.program_logic Require Export adequacy.
From iris.heap_lang Require Export lang notation tactics.
-From iris Require Import options.
+From iris.prelude Require Import options.
(** This file contains the proof that prophecies can be safely erased
from programs. We erase a program by replacing prophecy identifiers
diff --git a/theories/heap_lang/tactics.v b/iris_heap_lang/tactics.v
similarity index 98%
rename from theories/heap_lang/tactics.v
rename to iris_heap_lang/tactics.v
index 9b19bb9a638b24c9eef139c409bb07887535284e..f29521e8bdcc89984aa381418a37298067e148f4 100644
--- a/theories/heap_lang/tactics.v
+++ b/iris_heap_lang/tactics.v
@@ -1,5 +1,5 @@
From iris.heap_lang Require Export lang.
-From iris Require Import options.
+From iris.prelude Require Import options.
Import heap_lang.
(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
diff --git a/theories/heap_lang/total_adequacy.v b/iris_heap_lang/total_adequacy.v
similarity index 94%
rename from theories/heap_lang/total_adequacy.v
rename to iris_heap_lang/total_adequacy.v
index 4d07855593ec88efbcc91a0046d2187b26852055..cdda3d0677c776720b2ee81bc996d793460b1df7 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/iris_heap_lang/total_adequacy.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export total_adequacy.
From iris.heap_lang Require Export adequacy.
From iris.heap_lang Require Import proofmode notation.
-From iris Require Import options.
+From iris.prelude Require Import options.
Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
(∀ `{!heapG Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌠}]) →
diff --git a/make-package b/make-package
new file mode 100755
index 0000000000000000000000000000000000000000..55c051a9f6b9b3d25936782b46e6b55dc35fa4ab
--- /dev/null
+++ b/make-package
@@ -0,0 +1,32 @@
+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! egrep -q "^$PROJECT/" _CoqProject; then
+ echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+ exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+egrep "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | egrep -v "^-Q " >> "$COQFILE"
+# Get the files.
+egrep "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*