From 2ab9e4a25a16061f9a7ce4f3d344362d645d1f9a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 25 Sep 2020 17:34:14 +0200
Subject: [PATCH] multi-package repositories
---
.gitignore | 9 +-
.gitlab-ci.yml | 2 +-
Makefile.coq.local | 2 +-
_CoqProject | 308 +++++++++---------
coq-iris-heap-lang.opam | 16 +
coq-iris.opam | 4 +-
{theories => iris}/algebra/agree.v | 2 +-
{theories => iris}/algebra/auth.v | 2 +-
{theories => iris}/algebra/base.v | 2 +-
{theories => iris}/algebra/big_op.v | 2 +-
{theories => iris}/algebra/cmra.v | 2 +-
{theories => iris}/algebra/cmra_big_op.v | 2 +-
{theories => iris}/algebra/coPset.v | 2 +-
{theories => iris}/algebra/cofe_solver.v | 2 +-
{theories => iris}/algebra/csum.v | 2 +-
{theories => iris}/algebra/dfrac.v | 2 +-
{theories => iris}/algebra/dra.v | 2 +-
{theories => iris}/algebra/excl.v | 2 +-
{theories => iris}/algebra/frac.v | 2 +-
{theories => iris}/algebra/functions.v | 2 +-
{theories => iris}/algebra/gmap.v | 2 +-
{theories => iris}/algebra/gmultiset.v | 2 +-
{theories => iris}/algebra/gset.v | 2 +-
{theories => iris}/algebra/lib/excl_auth.v | 2 +-
{theories => iris}/algebra/lib/frac_agree.v | 2 +-
{theories => iris}/algebra/lib/frac_auth.v | 2 +-
{theories => iris}/algebra/lib/gmap_view.v | 2 +-
{theories => iris}/algebra/lib/mnat_auth.v | 2 +-
{theories => iris}/algebra/lib/ufrac_auth.v | 2 +-
{theories => iris}/algebra/list.v | 2 +-
{theories => iris}/algebra/local_updates.v | 2 +-
{theories => iris}/algebra/monoid.v | 2 +-
{theories => iris}/algebra/namespace_map.v | 2 +-
{theories => iris}/algebra/numbers.v | 2 +-
{theories => iris}/algebra/ofe.v | 2 +-
.../algebra/proofmode_classes.v | 2 +-
{theories => iris}/algebra/sts.v | 2 +-
{theories => iris}/algebra/ufrac.v | 2 +-
{theories => iris}/algebra/updates.v | 2 +-
{theories => iris}/algebra/vector.v | 2 +-
{theories => iris}/algebra/view.v | 2 +-
{theories => iris}/base_logic/algebra.v | 2 +-
{theories => iris}/base_logic/base_logic.v | 2 +-
{theories => iris}/base_logic/bi.v | 2 +-
{theories => iris}/base_logic/bupd_alt.v | 2 +-
{theories => iris}/base_logic/derived.v | 2 +-
{theories => iris}/base_logic/lib/auth.v | 2 +-
{theories => iris}/base_logic/lib/boxes.v | 2 +-
.../base_logic/lib/cancelable_invariants.v | 2 +-
.../base_logic/lib/fancy_updates.v | 2 +-
.../base_logic/lib/fancy_updates_from_vs.v | 2 +-
{theories => iris}/base_logic/lib/gen_heap.v | 2 +-
.../base_logic/lib/gen_inv_heap.v | 2 +-
{theories => iris}/base_logic/lib/ghost_var.v | 2 +-
.../base_logic/lib/invariants.v | 2 +-
{theories => iris}/base_logic/lib/iprop.v | 2 +-
{theories => iris}/base_logic/lib/mnat.v | 2 +-
.../base_logic/lib/na_invariants.v | 2 +-
{theories => iris}/base_logic/lib/own.v | 2 +-
{theories => iris}/base_logic/lib/proph_map.v | 2 +-
.../base_logic/lib/saved_prop.v | 2 +-
{theories => iris}/base_logic/lib/sts.v | 2 +-
.../base_logic/lib/viewshifts.v | 2 +-
{theories => iris}/base_logic/lib/wsat.v | 2 +-
{theories => iris}/base_logic/proofmode.v | 2 +-
{theories => iris}/base_logic/upred.v | 3 +-
{theories => iris}/bi/ascii.v | 2 +-
{theories => iris}/bi/bi.v | 2 +-
{theories => iris}/bi/big_op.v | 2 +-
{theories => iris}/bi/derived_connectives.v | 2 +-
{theories => iris}/bi/derived_laws.v | 2 +-
{theories => iris}/bi/derived_laws_later.v | 2 +-
{theories => iris}/bi/embedding.v | 2 +-
{theories => iris}/bi/interface.v | 2 +-
{theories => iris}/bi/internal_eq.v | 2 +-
{theories => iris}/bi/lib/atomic.v | 2 +-
{theories => iris}/bi/lib/core.v | 2 +-
{theories => iris}/bi/lib/counterexamples.v | 2 +-
{theories => iris}/bi/lib/fixpoint.v | 2 +-
{theories => iris}/bi/lib/fractional.v | 2 +-
{theories => iris}/bi/lib/laterable.v | 2 +-
{theories => iris}/bi/lib/relations.v | 2 +-
{theories => iris}/bi/monpred.v | 2 +-
{theories => iris}/bi/notation.v | 2 +-
{theories => iris}/bi/plainly.v | 2 +-
{theories => iris}/bi/telescopes.v | 2 +-
{theories => iris}/bi/updates.v | 2 +-
{theories => iris}/bi/weakestpre.v | 2 +-
{theories => iris/prelude}/options.v | 2 +-
{theories => iris}/program_logic/adequacy.v | 2 +-
{theories => iris}/program_logic/atomic.v | 2 +-
.../program_logic/ectx_language.v | 2 +-
.../program_logic/ectx_lifting.v | 2 +-
.../program_logic/ectxi_language.v | 2 +-
{theories => iris}/program_logic/hoare.v | 2 +-
{theories => iris}/program_logic/language.v | 2 +-
{theories => iris}/program_logic/lifting.v | 2 +-
{theories => iris}/program_logic/ownp.v | 2 +-
.../program_logic/total_adequacy.v | 2 +-
.../program_logic/total_ectx_lifting.v | 2 +-
.../program_logic/total_lifting.v | 2 +-
.../program_logic/total_weakestpre.v | 2 +-
{theories => iris}/program_logic/weakestpre.v | 2 +-
{theories => iris}/proofmode/base.v | 2 +-
.../proofmode/class_instances.v | 2 +-
.../proofmode/class_instances_embedding.v | 2 +-
.../proofmode/class_instances_internal_eq.v | 2 +-
.../proofmode/class_instances_later.v | 2 +-
.../proofmode/class_instances_plainly.v | 2 +-
.../proofmode/class_instances_updates.v | 2 +-
{theories => iris}/proofmode/classes.v | 2 +-
{theories => iris}/proofmode/coq_tactics.v | 2 +-
{theories => iris}/proofmode/environments.v | 2 +-
.../proofmode/frame_instances.v | 2 +-
{theories => iris}/proofmode/ident_name.v | 2 +-
{theories => iris}/proofmode/intro_patterns.v | 2 +-
{theories => iris}/proofmode/ltac_tactics.v | 2 +-
{theories => iris}/proofmode/modalities.v | 2 +-
.../proofmode/modality_instances.v | 2 +-
{theories => iris}/proofmode/monpred.v | 2 +-
{theories => iris}/proofmode/notation.v | 2 +-
{theories => iris}/proofmode/reduction.v | 2 +-
{theories => iris}/proofmode/sel_patterns.v | 2 +-
{theories => iris}/proofmode/spec_patterns.v | 2 +-
{theories => iris}/proofmode/tactics.v | 2 +-
{theories => iris}/proofmode/tokens.v | 2 +-
{theories => iris}/si_logic/bi.v | 2 +-
{theories => iris}/si_logic/siprop.v | 2 +-
.../heap_lang => iris_heap_lang}/adequacy.v | 2 +-
.../derived_laws.v | 2 +-
{theories/heap_lang => iris_heap_lang}/lang.v | 2 +-
.../heap_lang => iris_heap_lang}/lib/arith.v | 2 +-
.../heap_lang => iris_heap_lang}/lib/array.v | 2 +-
.../heap_lang => iris_heap_lang}/lib/assert.v | 2 +-
.../lib/atomic_heap.v | 2 +-
.../lib/clairvoyant_coin.v | 2 +-
.../lib/counter.v | 2 +-
.../lib/diverge.v | 2 +-
.../lib/increment.v | 2 +-
.../lib/lazy_coin.v | 2 +-
.../heap_lang => iris_heap_lang}/lib/lock.v | 2 +-
.../lib/nondet_bool.v | 2 +-
.../heap_lang => iris_heap_lang}/lib/par.v | 2 +-
.../heap_lang => iris_heap_lang}/lib/spawn.v | 2 +-
.../lib/spin_lock.v | 2 +-
.../lib/ticket_lock.v | 2 +-
.../heap_lang => iris_heap_lang}/locations.v | 2 +-
.../heap_lang => iris_heap_lang}/metatheory.v | 2 +-
.../heap_lang => iris_heap_lang}/notation.v | 2 +-
.../primitive_laws.v | 2 +-
.../heap_lang => iris_heap_lang}/proofmode.v | 2 +-
.../proph_erasure.v | 2 +-
.../heap_lang => iris_heap_lang}/tactics.v | 2 +-
.../total_adequacy.v | 2 +-
make-package | 27 ++
155 files changed, 361 insertions(+), 304 deletions(-)
create mode 100644 coq-iris-heap-lang.opam
rename {theories => iris}/algebra/agree.v (99%)
rename {theories => iris}/algebra/auth.v (99%)
rename {theories => iris}/algebra/base.v (82%)
rename {theories => iris}/algebra/big_op.v (99%)
rename {theories => iris}/algebra/cmra.v (99%)
rename {theories => iris}/algebra/cmra_big_op.v (97%)
rename {theories => iris}/algebra/coPset.v (99%)
rename {theories => iris}/algebra/cofe_solver.v (99%)
rename {theories => iris}/algebra/csum.v (99%)
rename {theories => iris}/algebra/dfrac.v (99%)
rename {theories => iris}/algebra/dra.v (99%)
rename {theories => iris}/algebra/excl.v (99%)
rename {theories => iris}/algebra/frac.v (98%)
rename {theories => iris}/algebra/functions.v (99%)
rename {theories => iris}/algebra/gmap.v (99%)
rename {theories => iris}/algebra/gmultiset.v (98%)
rename {theories => iris}/algebra/gset.v (99%)
rename {theories => iris}/algebra/lib/excl_auth.v (98%)
rename {theories => iris}/algebra/lib/frac_agree.v (98%)
rename {theories => iris}/algebra/lib/frac_auth.v (99%)
rename {theories => iris}/algebra/lib/gmap_view.v (99%)
rename {theories => iris}/algebra/lib/mnat_auth.v (98%)
rename {theories => iris}/algebra/lib/ufrac_auth.v (99%)
rename {theories => iris}/algebra/list.v (99%)
rename {theories => iris}/algebra/local_updates.v (99%)
rename {theories => iris}/algebra/monoid.v (98%)
rename {theories => iris}/algebra/namespace_map.v (99%)
rename {theories => iris}/algebra/numbers.v (99%)
rename {theories => iris}/algebra/ofe.v (99%)
rename {theories => iris}/algebra/proofmode_classes.v (98%)
rename {theories => iris}/algebra/sts.v (99%)
rename {theories => iris}/algebra/ufrac.v (97%)
rename {theories => iris}/algebra/updates.v (99%)
rename {theories => iris}/algebra/vector.v (98%)
rename {theories => iris}/algebra/view.v (99%)
rename {theories => iris}/base_logic/algebra.v (99%)
rename {theories => iris}/base_logic/base_logic.v (90%)
rename {theories => iris}/base_logic/bi.v (99%)
rename {theories => iris}/base_logic/bupd_alt.v (99%)
rename {theories => iris}/base_logic/derived.v (98%)
rename {theories => iris}/base_logic/lib/auth.v (99%)
rename {theories => iris}/base_logic/lib/boxes.v (99%)
rename {theories => iris}/base_logic/lib/cancelable_invariants.v (99%)
rename {theories => iris}/base_logic/lib/fancy_updates.v (99%)
rename {theories => iris}/base_logic/lib/fancy_updates_from_vs.v (98%)
rename {theories => iris}/base_logic/lib/gen_heap.v (99%)
rename {theories => iris}/base_logic/lib/gen_inv_heap.v (99%)
rename {theories => iris}/base_logic/lib/ghost_var.v (98%)
rename {theories => iris}/base_logic/lib/invariants.v (99%)
rename {theories => iris}/base_logic/lib/iprop.v (99%)
rename {theories => iris}/base_logic/lib/mnat.v (99%)
rename {theories => iris}/base_logic/lib/na_invariants.v (99%)
rename {theories => iris}/base_logic/lib/own.v (99%)
rename {theories => iris}/base_logic/lib/proph_map.v (99%)
rename {theories => iris}/base_logic/lib/saved_prop.v (99%)
rename {theories => iris}/base_logic/lib/sts.v (99%)
rename {theories => iris}/base_logic/lib/viewshifts.v (98%)
rename {theories => iris}/base_logic/lib/wsat.v (99%)
rename {theories => iris}/base_logic/proofmode.v (97%)
rename {theories => iris}/base_logic/upred.v (99%)
rename {theories => iris}/bi/ascii.v (99%)
rename {theories => iris}/bi/bi.v (85%)
rename {theories => iris}/bi/big_op.v (99%)
rename {theories => iris}/bi/derived_connectives.v (99%)
rename {theories => iris}/bi/derived_laws.v (99%)
rename {theories => iris}/bi/derived_laws_later.v (99%)
rename {theories => iris}/bi/embedding.v (99%)
rename {theories => iris}/bi/interface.v (99%)
rename {theories => iris}/bi/internal_eq.v (99%)
rename {theories => iris}/bi/lib/atomic.v (99%)
rename {theories => iris}/bi/lib/core.v (98%)
rename {theories => iris}/bi/lib/counterexamples.v (99%)
rename {theories => iris}/bi/lib/fixpoint.v (99%)
rename {theories => iris}/bi/lib/fractional.v (99%)
rename {theories => iris}/bi/lib/laterable.v (99%)
rename {theories => iris}/bi/lib/relations.v (98%)
rename {theories => iris}/bi/monpred.v (99%)
rename {theories => iris}/bi/notation.v (99%)
rename {theories => iris}/bi/plainly.v (99%)
rename {theories => iris}/bi/telescopes.v (98%)
rename {theories => iris}/bi/updates.v (99%)
rename {theories => iris}/bi/weakestpre.v (99%)
rename {theories => iris/prelude}/options.v (93%)
rename {theories => iris}/program_logic/adequacy.v (99%)
rename {theories => iris}/program_logic/atomic.v (99%)
rename {theories => iris}/program_logic/ectx_language.v (99%)
rename {theories => iris}/program_logic/ectx_lifting.v (99%)
rename {theories => iris}/program_logic/ectxi_language.v (99%)
rename {theories => iris}/program_logic/hoare.v (99%)
rename {theories => iris}/program_logic/language.v (99%)
rename {theories => iris}/program_logic/lifting.v (99%)
rename {theories => iris}/program_logic/ownp.v (99%)
rename {theories => iris}/program_logic/total_adequacy.v (99%)
rename {theories => iris}/program_logic/total_ectx_lifting.v (98%)
rename {theories => iris}/program_logic/total_lifting.v (98%)
rename {theories => iris}/program_logic/total_weakestpre.v (99%)
rename {theories => iris}/program_logic/weakestpre.v (99%)
rename {theories => iris}/proofmode/base.v (98%)
rename {theories => iris}/proofmode/class_instances.v (99%)
rename {theories => iris}/proofmode/class_instances_embedding.v (99%)
rename {theories => iris}/proofmode/class_instances_internal_eq.v (98%)
rename {theories => iris}/proofmode/class_instances_later.v (99%)
rename {theories => iris}/proofmode/class_instances_plainly.v (99%)
rename {theories => iris}/proofmode/class_instances_updates.v (99%)
rename {theories => iris}/proofmode/classes.v (99%)
rename {theories => iris}/proofmode/coq_tactics.v (99%)
rename {theories => iris}/proofmode/environments.v (99%)
rename {theories => iris}/proofmode/frame_instances.v (99%)
rename {theories => iris}/proofmode/ident_name.v (97%)
rename {theories => iris}/proofmode/intro_patterns.v (99%)
rename {theories => iris}/proofmode/ltac_tactics.v (99%)
rename {theories => iris}/proofmode/modalities.v (99%)
rename {theories => iris}/proofmode/modality_instances.v (98%)
rename {theories => iris}/proofmode/monpred.v (99%)
rename {theories => iris}/proofmode/notation.v (97%)
rename {theories => iris}/proofmode/reduction.v (97%)
rename {theories => iris}/proofmode/sel_patterns.v (96%)
rename {theories => iris}/proofmode/spec_patterns.v (98%)
rename {theories => iris}/proofmode/tactics.v (90%)
rename {theories => iris}/proofmode/tokens.v (98%)
rename {theories => iris}/si_logic/bi.v (99%)
rename {theories => iris}/si_logic/siprop.v (99%)
rename {theories/heap_lang => iris_heap_lang}/adequacy.v (96%)
rename {theories/heap_lang => iris_heap_lang}/derived_laws.v (99%)
rename {theories/heap_lang => iris_heap_lang}/lang.v (99%)
rename {theories/heap_lang => iris_heap_lang}/lib/arith.v (97%)
rename {theories/heap_lang => iris_heap_lang}/lib/array.v (99%)
rename {theories/heap_lang => iris_heap_lang}/lib/assert.v (95%)
rename {theories/heap_lang => iris_heap_lang}/lib/atomic_heap.v (99%)
rename {theories/heap_lang => iris_heap_lang}/lib/clairvoyant_coin.v (98%)
rename {theories/heap_lang => iris_heap_lang}/lib/counter.v (99%)
rename {theories/heap_lang => iris_heap_lang}/lib/diverge.v (96%)
rename {theories/heap_lang => iris_heap_lang}/lib/increment.v (99%)
rename {theories/heap_lang => iris_heap_lang}/lib/lazy_coin.v (97%)
rename {theories/heap_lang => iris_heap_lang}/lib/lock.v (97%)
rename {theories/heap_lang => iris_heap_lang}/lib/nondet_bool.v (94%)
rename {theories/heap_lang => iris_heap_lang}/lib/par.v (97%)
rename {theories/heap_lang => iris_heap_lang}/lib/spawn.v (98%)
rename {theories/heap_lang => iris_heap_lang}/lib/spin_lock.v (99%)
rename {theories/heap_lang => iris_heap_lang}/lib/ticket_lock.v (99%)
rename {theories/heap_lang => iris_heap_lang}/locations.v (97%)
rename {theories/heap_lang => iris_heap_lang}/metatheory.v (99%)
rename {theories/heap_lang => iris_heap_lang}/notation.v (99%)
rename {theories/heap_lang => iris_heap_lang}/primitive_laws.v (99%)
rename {theories/heap_lang => iris_heap_lang}/proofmode.v (99%)
rename {theories/heap_lang => iris_heap_lang}/proph_erasure.v (99%)
rename {theories/heap_lang => iris_heap_lang}/tactics.v (98%)
rename {theories/heap_lang => iris_heap_lang}/total_adequacy.v (94%)
create mode 100755 make-package
diff --git a/.gitignore b/.gitignore
index bfd0941de..fead3cd9c 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 8e82fc715..414e1f503 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/Makefile.coq.local b/Makefile.coq.local
index 9ff769d27..4d24c334b 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/_CoqProject b/_CoqProject
index 37fc08f79..598e82936 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 000000000..d0cfb0627
--- /dev/null
+++ b/coq-iris-heap-lang.opam
@@ -0,0 +1,16 @@
+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"
+
+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 fd8bf766b..b4c61440f 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -13,5 +13,5 @@ depends: [
"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 c0ae62c91..f5733133f 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 6adb6c2e4..29c5c0ae5 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 3341e502c..d915dfc3f 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 18c6eaa28..92a790f25 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 cfc26604a..3f8f002a1 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 37ae37931..73e7d22f3 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 dcd07527b..872cbfb87 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 9330d77eb..948c57c22 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 74d83490b..e0e5ce8fe 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 5fadf0e77..4006adc93 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 1e8902001..5d8679358 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 10a86de74..c5d9ef110 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 ad8ac9ba0..6135787f1 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 dd40746ec..98f36dfbd 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 bc89495cc..dc39ca0fe 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 4bbb9cf8d..5e2f02f28 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 832616e9d..c95e6c370 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 307a841cc..c410935a6 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 af00e2bf8..6812ca9a6 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 6174a3e54..b3bed379c 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 0be0eaf46..4c30f0144 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 aa3c062eb..351fa0a2f 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 1f5705f2d..e7f1f0a39 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 798a80daa..363a06e51 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 92110f0b2..c662b4229 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 0c7a2e5f5..f8a563322 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 98656d914..aae353ecb 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 0d73b1199..fa74e1172 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 0b0963f54..135865d7e 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 7cfbdc09b..efd07f08a 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 fae53edbd..65257373f 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 12bcf2e9f..12cb72449 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 d98af92a1..1a671def3 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 17f964f61..dd2a27c39 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 e8ad6e623..3a02bf95a 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 c8d95b720..35a40a4ee 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 2c4446953..66c98d955 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 fa2327ae6..ad6814fb4 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 307f38850..efb542d4c 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 192810f68..ad9a4c01e 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 2d99ad3c1..5733f9aa4 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 cad377165..8f0620e03 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 0a4407c19..5ad576c95 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 558fae055..7bdce06e5 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 f1c0ccc10..a3d331e04 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 73d9aa5a5..1963deca9 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 b180bb9b6..da0667462 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 c3592a927..9c17c521a 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 5fa9cd8d0..e7cc9b638 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 a40c6d1cf..36a4fdd4f 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 b25f4358d..b8f554888 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 9f3f659ce..f4874e831 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 3417797d8..e95e32e79 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 19cacccd9..d12feb530 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 f9915ee2b..1038d4d71 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 329ead42a..d4e4f8680 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 04b335836..5aa7b55e2 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 c64dcebcd..d33c9105b 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 04d05d104..dfebe0742 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 445ad37ba..bdb236c4e 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 434592fd9..287866f6b 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 66afc4ad7..f9ef24760 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 2f260da12..09ac481d1 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 671a8ae13..88e7dcca5 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 aab10e497..8f7c63fd0 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 85b375a2c..3f61a09c4 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 bb73cf16a..354028caa 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 dc7155fb2..f3f66ba4f 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 df3f1a817..4562e5871 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 d79d71a85..2658652ec 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 dc67214dc..3d2380430 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 de6465eca..23a96554f 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 8935289d8..9ca541ab8 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 4d4b9ffa5..644c47ef2 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 eaac68789..1d11af00c 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 11f5d6aa7..1d1d09ffe 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 f2bb21e9a..d1f047eb4 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 bea7f6b41..117ced195 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 c35d74379..4d2439693 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 2bef8b0e7..b2836192c 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 0674386ab..65b06d251 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 ee7181d5c..75963fa02 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 1e4c1f311..22d74e4a4 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 612af7f29..ef2abff21 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 13be0ce35..04a07d03e 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 ebf94a867..a76f590ed 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 926ae75c5..11372d1c7 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 e9e9477c5..e3a245b2e 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 b08d144fb..45f9702cd 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 603391006..c599f97c9 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 bb5fa43d6..9b532e703 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 78e6ffcf9..9b8e438be 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 1825b3cd9..19ffe2810 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 99c34b6d3..2d0d1043d 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 19b9af5a2..c1e4eb617 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 1fa5c0324..e1aa91555 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 e0d639fb6..a80ee8512 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 abf4e1361..5a969fea0 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 502326653..8b5f315fb 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 c75f27534..e355153ea 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 c75ead317..a8cf210e7 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 ffab7068c..d4c7e2d3a 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 f3eba370e..b49f42a76 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 9bc9f38aa..0e0a116d5 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 9c1d7af95..b71455cd7 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 3987d63bc..5aee11b50 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 e77b6b44e..e185690dc 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 11c96ddcc..291e326b7 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 136493f13..709205e3e 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 d5895ebdc..4847e2aca 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 6cd5e2e4c..5cb16a875 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 cc33f63bd..1e65317da 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 23d93c65e..ea0d67984 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 e9012f268..f59f09245 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 d2812ef7a..0f4fd26c0 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 c92ba206b..b70aef0a3 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 0b360c196..6f498a365 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 b2edc3b4c..983b6d260 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 6fdca9b1e..f7680f074 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 b7d075007..a450d6c2f 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 6dbcd41a3..dc8be0254 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 30343ff49..345994a21 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 ed24c8ae3..a1d218d3d 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 4a394f6b6..addf300ba 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 7d4f4f0b5..226b4e183 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 501cfbabc..8a2165ce6 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 f7e2bd7bd..40f8387df 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 db8adb8d6..1397a3380 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 f39fc9d07..0679e493f 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 70673ad50..e840732bb 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 48537d024..378b03fcf 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 393445f46..18a27c2f2 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 bf71e6f3b..604ecac1b 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 315cc5f3f..588380e97 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 8edd581e4..c34a77368 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 98aec67e0..f81d48cce 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 fb33eb800..ad4046100 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 0d033c5d1..8be6983d5 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 8f4986496..a847b985a 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 5b202eaed..55856b304 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 146b3816a..7cca50788 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 106a12423..54619aa4a 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 f9948af37..6ea7e8eaa 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 ce297d8e6..36deec1e8 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 6eaf109e1..8826570fa 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 4cfeef1bc..750b55bd4 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 9b19bb9a6..f29521e8b 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 4d0785559..cdda3d067 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 000000000..028220c0d
--- /dev/null
+++ b/make-package
@@ -0,0 +1,27 @@
+#!/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"
+
+# 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"*
--
GitLab