diff --git a/_CoqProject b/_CoqProject
index c179fb492bbf56bca55d0f90ff0d036fcbaeadc4..aedb367b88fc3f7f6d1ecf4c6d28f0dabd7db2ea 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,4 @@
--Q . ""
+-Q . iris
 prelude/option.v
 prelude/fin_map_dom.v
 prelude/bsets.v
diff --git a/algebra/agree.v b/algebra/agree.v
index 4039c7e40daece079173718fd94f5d2258b1c2c7..cab28bc9494e80a8df94fe614b00b3d378ca042c 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -1,5 +1,5 @@
-From algebra Require Export cmra.
-From algebra Require Import upred.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import upred.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
diff --git a/algebra/auth.v b/algebra/auth.v
index f341742923ce6118d90fed813aaf9efc7a12d7d8..e2e54fb184de6553c0ab55a74dbf421d0c286b6d 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,5 +1,5 @@
-From algebra Require Export excl.
-From algebra Require Import upred.
+From iris.algebra Require Export excl.
+From iris.algebra Require Import upred.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
diff --git a/algebra/base.v b/algebra/base.v
index 5235048e27407546fdfa3d668df21e503b052d9a..483d63d721fa48c6111edc302facda9fee12731d 100644
--- a/algebra/base.v
+++ b/algebra/base.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect.
-From prelude Require Export prelude.
+From iris.prelude Require Export prelude.
 Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.
 Ltac done := prelude.tactics.done.
\ No newline at end of file
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 8725d9665575cc08218052e85a482656ef7e9473..08256da86301ae6a933c88c94bb9282818c51a7e 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1,4 +1,4 @@
-From algebra Require Export cofe.
+From iris.algebra Require Export cofe.
 
 Class Core (A : Type) := core : A → A.
 Instance: Params (@core) 2.
diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 3094846eafe761aac45d1fd133e613f43a57178f..2e3d894e697aa8c1389696d05d14a7ad6e6cb12c 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -1,5 +1,5 @@
-From algebra Require Export cmra.
-From prelude Require Import gmap.
+From iris.algebra Require Export cmra.
+From iris.prelude Require Import gmap.
 
 Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
   match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
diff --git a/algebra/cmra_tactics.v b/algebra/cmra_tactics.v
index 342c0ba85db3b9e8bd4b85db82a55fcb73394f02..6943f64bf58b9c3900bd48fbfb761e2d400fb7c2 100644
--- a/algebra/cmra_tactics.v
+++ b/algebra/cmra_tactics.v
@@ -1,5 +1,5 @@
-From algebra Require Export cmra.
-From algebra Require Import cmra_big_op.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import cmra_big_op.
 
 (** * Simple solver for validity and inclusion by reflection *)
 Module ra_reflection. Section ra_reflection.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index b1bf310324209bec3d7716dfbc14e9642a5dff28..0e880514d5916be96d17daaa088c2ed938034712 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -1,4 +1,4 @@
-From algebra Require Export base.
+From iris.algebra Require Export base.
 
 (** This files defines (a shallow embedding of) the category of COFEs:
     Complete ordered families of equivalences. This is a cartesian closed
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 855db70a11dc55bcaade42828042f531e3df6027..280dce025a9e92c1d4eb88622ad4ab1bcc97d016 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -1,4 +1,4 @@
-From algebra Require Export cofe.
+From iris.algebra Require Export cofe.
 
 Record solution (F : cFunctor) := Solution {
   solution_car :> cofeT;
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 202b80ffad0627002776b646e1960cfdcc63e921..b7c37089aca2a0cddb780ba4a745312ebe34a29e 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -1,4 +1,4 @@
-From algebra Require Export cmra.
+From iris.algebra Require Export cmra.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
diff --git a/algebra/dra.v b/algebra/dra.v
index 1909b430a12445c24b9cc5a13e7c9022f7ec6ced..36fe74bb7bcf428637e57fc4985698bb7c2968ff 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -1,4 +1,4 @@
-From algebra Require Export cmra.
+From iris.algebra Require Export cmra.
 
 (** From disjoint pcm *)
 Record validity {A} (P : A → Prop) : Type := Validity {
diff --git a/algebra/excl.v b/algebra/excl.v
index 884c01a02d4e36a4c3f0954b095e405ba123e016..9f731370e9dad3262162d3f11eb7d21493bd3b9a 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -1,5 +1,5 @@
-From algebra Require Export cmra.
-From algebra Require Import upred.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 28fa2fe7a501485f1d15bb670260a18c50471090..0215ded5026d03defce89006b6b87ff8c7d66719 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -1,6 +1,6 @@
-From algebra Require Export cmra option.
-From prelude Require Export gmap.
-From algebra Require Import upred.
+From iris.algebra Require Export cmra option.
+From iris.prelude Require Export gmap.
+From iris.algebra Require Import upred.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
diff --git a/algebra/frac.v b/algebra/frac.v
index e2e609f7ca05016b8fa411d8b0156ff318a9975d..daf952db352e6540dd924c80ab7fead6dfb7fdf2 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
-From algebra Require Export cmra.
-From algebra Require Import upred.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments div _ _ !_ !_ /.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index abf208ab58b1dc54dc3c0e2fa0109c3358c36048..34f4dcac53d3bca0d989eabb1b7a59b79c46000e 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -1,5 +1,5 @@
-From algebra Require Export cmra.
-From algebra Require Import upred.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import upred.
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
diff --git a/algebra/option.v b/algebra/option.v
index ba5b87fea54f7a5a20d2afec1278bce729471309..1530ecd6ec9484f8e2c3f9a6745505ffa31a81aa 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -1,5 +1,5 @@
-From algebra Require Export cmra.
-From algebra Require Import upred.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import upred.
 
 (* COFE *)
 Section cofe.
diff --git a/algebra/sts.v b/algebra/sts.v
index 5a1fc8bd62d1efcb9292750cd53c4812915944f0..216f7bd0ede200867abccff9e08cc0bcd1d99e60 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -1,6 +1,6 @@
-From prelude Require Export sets.
-From algebra Require Export cmra.
-From algebra Require Import dra.
+From iris.prelude Require Export sets.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import dra.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
diff --git a/algebra/upred.v b/algebra/upred.v
index 306906368165bc7ad6313ad46f908e682621504a..968d89add18fec3076a7297e8d15d3122d1a6224 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1,4 +1,4 @@
-From algebra Require Export cmra.
+From iris.algebra Require Export cmra.
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index b8ac2cd8f66b7d8f2c644f97a15af3009e160b9a..d9e700cb35b1177902e865f4ad20ffb06465b074 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -1,5 +1,5 @@
-From algebra Require Export upred.
-From prelude Require Import gmap fin_collections.
+From iris.algebra Require Export upred.
+From iris.prelude Require Import gmap fin_collections.
 Import uPred.
 
 (** * Big ops over lists *)
diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index b8c9368bcaa02a8dba5146c565099ad0237c7ed7..5fc479b605dfa96201de5f687a44971505712c29 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -1,5 +1,5 @@
-From algebra Require Export upred.
-From algebra Require Export upred_big_op.
+From iris.algebra Require Export upred.
+From iris.algebra Require Export upred_big_op.
 Import uPred.
 
 Module uPred_reflection. Section uPred_reflection.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index d9dd2b4e60b1d4f7e04b4e8ab85d89439c086a5e..d8e4a6618c5d54172c91b48ebbbf5d69a65e7b21 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -1,4 +1,4 @@
-From heap_lang Require Export notation.
+From iris.heap_lang Require Export notation.
 
 Definition newbarrier : val := λ: <>, ref #0.
 Definition signal : val := λ: "x", '"x" <- #1.
diff --git a/barrier/client.v b/barrier/client.v
index 57465a50d0052a5beee888018170b2723275a9cc..c630e7da05f3a23d6ddfa94d2c529c1d7068778f 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -1,6 +1,6 @@
-From barrier Require Import proof.
-From heap_lang Require Import par.
-From program_logic Require Import auth sts saved_prop hoare ownership.
+From iris.barrier Require Import proof.
+From iris.heap_lang Require Import par.
+From iris.program_logic Require Import auth sts saved_prop hoare ownership.
 Import uPred.
 
 Definition worker (n : Z) : val :=
diff --git a/barrier/proof.v b/barrier/proof.v
index ac18c35cfd4b9995395887708313a245a9de408b..40b99c0ade2c1ae5b6c41d4d8ab7ea628e0e90fe 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -1,9 +1,9 @@
-From prelude Require Import functions.
-From algebra Require Import upred_big_op.
-From program_logic Require Import sts saved_prop tactics.
-From heap_lang Require Export heap wp_tactics.
-From barrier Require Export barrier.
-From barrier Require Import protocol.
+From iris.prelude Require Import functions.
+From iris.algebra Require Import upred_big_op.
+From iris.program_logic Require Import sts saved_prop tactics.
+From iris.heap_lang Require Export heap wp_tactics.
+From iris.barrier Require Export barrier.
+From iris.barrier Require Import protocol.
 Import uPred.
 
 (** The CMRAs we need. *)
diff --git a/barrier/protocol.v b/barrier/protocol.v
index 53b315536f1382a066285f0cfb8b5cbca672ebef..4294c9e3279eeb55a04445a807285bc66face4b6 100644
--- a/barrier/protocol.v
+++ b/barrier/protocol.v
@@ -1,5 +1,5 @@
-From algebra Require Export sts.
-From program_logic Require Import ghost_ownership.
+From iris.algebra Require Export sts.
+From iris.program_logic Require Import ghost_ownership.
 
 (** The STS describing the main barrier protocol. Every state has an index-set
     associated with it. These indices are actually [gname], because we use them
diff --git a/barrier/specification.v b/barrier/specification.v
index 8de9c66e36236626216af1f9c3268a10f3d17ef8..2f57dc41d98aba127016c3fae8239e9ca722b329 100644
--- a/barrier/specification.v
+++ b/barrier/specification.v
@@ -1,6 +1,6 @@
-From program_logic Require Export hoare.
-From barrier Require Export barrier.
-From barrier Require Import proof.
+From iris.program_logic Require Export hoare.
+From iris.barrier Require Export barrier.
+From iris.barrier Require Import proof.
 Import uPred.
 
 Section spec.
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 4760925d59b3347d518dab406a8fc273676bd229..327bb7cc431823e0de931615ffb59918bf4ade1c 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -1,4 +1,4 @@
-From heap_lang Require Export lifting.
+From iris.heap_lang Require Export lifting.
 Import uPred.
 
 (** Define some derived forms, and derived lemmas about them. *)
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 4ca6c7dd3aa1090fc252b14e1b7eccadbc49cca9..7f31f37b54206545ea9fe15027f778f038e852d4 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,7 +1,7 @@
-From heap_lang Require Export lifting.
-From algebra Require Import upred_big_op frac dec_agree.
-From program_logic Require Export invariants ghost_ownership.
-From program_logic Require Import ownership auth.
+From iris.heap_lang Require Export lifting.
+From iris.algebra Require Import upred_big_op frac dec_agree.
+From iris.program_logic Require Export invariants ghost_ownership.
+From iris.program_logic Require Import ownership auth.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index bc135938a1e132b19348af4eb94dd39325ccb0e7..3d63e057b9cf05a4e062651fcdda34db7bd06ebb 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -1,6 +1,6 @@
-From program_logic Require Export language.
-From prelude Require Export strings.
-From prelude Require Import gmap.
+From iris.program_logic Require Export language.
+From iris.prelude Require Export strings.
+From iris.prelude Require Import gmap.
 
 Module heap_lang.
 Open Scope Z_scope.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 0e0edce3f7e366d3e18294f35351958053791d18..5df7f53b56a627f6e7851e889a4335c8dfe6a93b 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,8 +1,8 @@
-From program_logic Require Export weakestpre.
-From heap_lang Require Export lang.
-From program_logic Require Import lifting.
-From program_logic Require Import ownership. (* for ownP *)
-From heap_lang Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.program_logic Require Import lifting.
+From iris.program_logic Require Import ownership. (* for ownP *)
+From iris.heap_lang Require Import tactics.
 Import uPred.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 7ac1a85e78e85e615904f2ee6cfdcfeaef352a23..200cccb7d1c1c20d382a11993f1d1d12608d9312 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -1,4 +1,4 @@
-From heap_lang Require Export derived.
+From iris.heap_lang Require Export derived.
 Export heap_lang.
 
 Arguments wp {_ _} _ _%E _.
diff --git a/heap_lang/par.v b/heap_lang/par.v
index b3b9d1f9db9409b66a3cc2a41e106892fa4229be..f65ac187fcba3059751689a55f4cc436b8f3f5ff 100644
--- a/heap_lang/par.v
+++ b/heap_lang/par.v
@@ -1,5 +1,5 @@
-From heap_lang Require Export heap spawn.
-From heap_lang Require Import wp_tactics notation.
+From iris.heap_lang Require Export heap spawn.
+From iris.heap_lang Require Import wp_tactics notation.
 Import uPred.
 
 Definition par : val :=
diff --git a/heap_lang/spawn.v b/heap_lang/spawn.v
index c26c69590336f8610cd619be72acd2ba491ec099..e3db4ef0e14b1d7198754e597151ed64ee2c19a9 100644
--- a/heap_lang/spawn.v
+++ b/heap_lang/spawn.v
@@ -1,6 +1,6 @@
-From program_logic Require Export global_functor.
-From heap_lang Require Export heap.
-From heap_lang Require Import wp_tactics notation.
+From iris.program_logic Require Export global_functor.
+From iris.heap_lang Require Export heap.
+From iris.heap_lang Require Import wp_tactics notation.
 Import uPred.
 
 Definition spawn : val :=
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 7f854cbb465dc2ab1f258dbf67fa3b36f5071f1b..5ecd40c6b68ba13921acf1da79bb5eaf4b0d6481 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -1,4 +1,4 @@
-From heap_lang Require Export lang.
+From iris.heap_lang Require Export lang.
 Import heap_lang.
 
 (** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 441e59614183dacaf7e4ada0cfb397dbd6292e78..1fea861c4e57bb05ae126a68ade0cf72ee03c883 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -1,5 +1,5 @@
-From heap_lang Require Export substitution.
-From prelude Require Import fin_maps.
+From iris.heap_lang Require Export substitution.
+From iris.prelude Require Import fin_maps.
 Import heap_lang.
 
 (** The tactic [inv_step] performs inversion on hypotheses of the shape
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 95ddc3f1b06a9d6693f1625a9ba17771e0c42437..ce5d9c930668964ac2b4590a5ea50be39ac606a1 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,6 +1,6 @@
 (** This file is essentially a bunch of testcases. *)
-From program_logic Require Import ownership hoare auth.
-From heap_lang Require Import wp_tactics heap notation.
+From iris.program_logic Require Import ownership hoare auth.
+From iris.heap_lang Require Import wp_tactics heap notation.
 Import uPred.
 
 Section LangTests.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 9a4fc625357642e77731ae6fd2cf5de5eac68451..8d438899ad7d89cf65cb82d54f81aea9362120a2 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -1,5 +1,5 @@
-From algebra Require Export upred_tactics.
-From heap_lang Require Export tactics derived substitution.
+From iris.algebra Require Export upred_tactics.
+From iris.heap_lang Require Export tactics derived substitution.
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/prelude/bsets.v b/prelude/bsets.v
index 40216c1a3043e7371390de9f7a3ba203bdf9a75a..f0da19b3536a1ba684fb78914cfe10761eef99c5 100644
--- a/prelude/bsets.v
+++ b/prelude/bsets.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements bsets as functions into Prop. *)
-From prelude Require Export prelude.
+From iris.prelude Require Export prelude.
 
 Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
 Arguments mkBSet {_} _.
diff --git a/prelude/co_pset.v b/prelude/co_pset.v
index d2feb82036b2725d6b639076fe55b49a27212d10..80a7506976dca7aa4d276be65a4967264e32a0eb 100644
--- a/prelude/co_pset.v
+++ b/prelude/co_pset.v
@@ -2,8 +2,8 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This files implements an efficient implementation of finite/cofinite sets
 of positive binary naturals [positive]. *)
-From prelude Require Export collections.
-From prelude Require Import pmap gmap mapset.
+From iris.prelude Require Export collections.
+From iris.prelude Require Import pmap gmap mapset.
 Local Open Scope positive_scope.
 
 (** * The tree data structure *)
diff --git a/prelude/collections.v b/prelude/collections.v
index 13bba4fea9e5caa8713de6640bf47ef73328e48e..ed72cdd0c0b106860b2848a07b22a647a7051c53 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -3,7 +3,7 @@
 (** This file collects definitions and theorems on collections. Most
 importantly, it implements some tactics to automatically solve goals involving
 collections. *)
-From prelude Require Export base tactics orders.
+From iris.prelude Require Export base tactics orders.
 
 Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
diff --git a/prelude/countable.v b/prelude/countable.v
index 4db31897472e3f3ad34b6a646870cd88f99502f3..6267748cf967cdf4b5a1d987cd0cfe718a50220e 100644
--- a/prelude/countable.v
+++ b/prelude/countable.v
@@ -1,6 +1,6 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From prelude Require Export list.
+From iris.prelude Require Export list.
 Local Open Scope positive.
 
 Class Countable A `{∀ x y : A, Decision (x = y)} := {
diff --git a/prelude/decidable.v b/prelude/decidable.v
index d57c025c53732d4acd597e4251ff573579aba5cb..4dfd94a3753a8616dc321cf48bf6f3c52a303fde 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -3,7 +3,7 @@
 (** This file collects theorems, definitions, tactics, related to propositions
 with a decidable equality. Such propositions are collected by the [Decision]
 type class. *)
-From prelude Require Export proof_irrel.
+From iris.prelude Require Export proof_irrel.
 
 Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
 
diff --git a/prelude/error.v b/prelude/error.v
index bed968e6ce9526b8c262e3a5e5fd26291588c4aa..cba02173936c85202032ba143da8372248840fe4 100644
--- a/prelude/error.v
+++ b/prelude/error.v
@@ -1,6 +1,6 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From prelude Require Export list.
+From iris.prelude Require Export list.
 
 Definition error (S E A : Type) : Type := S → E + (A * S).
 
diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 65850cbf1ba205e73cebdf4a17935093ae08fcd5..5fafe28d53bc3cb2a4d1669e40fb6fdb8b7d9ddd 100644
--- a/prelude/fin_collections.v
+++ b/prelude/fin_collections.v
@@ -4,8 +4,8 @@
 importantly, it implements a fold and size function and some useful induction
 principles on finite collections . *)
 From Coq Require Import Permutation.
-From prelude Require Import relations listset.
-From prelude Require Export numbers collections.
+From iris.prelude Require Import relations listset.
+From iris.prelude Require Export numbers collections.
 
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
 Definition collection_fold `{Elements A C} {B}
diff --git a/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index 0d735863b03dcbf01e7624f3d6f73ef41f4b6a01..62b356ab4c6d0c20d6ff5a73fb413dbb8cc753cd 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/fin_map_dom.v
@@ -3,7 +3,7 @@
 (** This file provides an axiomatization of the domain function of finite
 maps. We provide such an axiomatization, instead of implementing the domain
 function in a generic way, to allow more efficient implementations. *)
-From prelude Require Export collections fin_maps.
+From iris.prelude Require Export collections fin_maps.
 
 Class FinMapDom K M D `{FMap M,
     ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 81ad3e2c07ac9e59561bb6647b186f9b461f9552..ba5dab026a0685ece29b81b7af48c8ff48347f3b 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful
 induction principles for finite maps and implements the tactic
 [simplify_map_eq] to simplify goals involving finite maps. *)
 From Coq Require Import Permutation.
-From prelude Require Export relations vector orders.
+From iris.prelude Require Export relations vector orders.
 
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
diff --git a/prelude/finite.v b/prelude/finite.v
index 4075de942d5cbf4c2f40408410b77c6c43cc2df3..02a0f84a54bd84ead3dcb304dc529c7f12501b6d 100644
--- a/prelude/finite.v
+++ b/prelude/finite.v
@@ -1,6 +1,6 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From prelude Require Export countable list.
+From iris.prelude Require Export countable list.
 
 Class Finite A `{∀ x y : A, Decision (x = y)} := {
   enum : list A;
diff --git a/prelude/functions.v b/prelude/functions.v
index 4842faa626e01a2dc7802273a4d59cb4af84ab50..1ae5080e7b26a2b24c0544cf33d9d6e47fda6afc 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -1,4 +1,4 @@
-From prelude Require Export base tactics.
+From iris.prelude Require Export base tactics.
 
 Section definitions.
   Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
diff --git a/prelude/gmap.v b/prelude/gmap.v
index c062478e4d7bf7abc0b803676949b999ee67273c..d595773207f32f154e59867cfd3e1598eac4b769 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -2,8 +2,8 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements finite maps and finite sets with keys of any countable
 type. The implementation is based on [Pmap]s, radix-2 search trees. *)
-From prelude Require Export countable fin_maps fin_map_dom.
-From prelude Require Import pmap mapset sets.
+From iris.prelude Require Export countable fin_maps fin_map_dom.
+From iris.prelude Require Import pmap mapset sets.
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
diff --git a/prelude/hashset.v b/prelude/hashset.v
index e5779a2fd23e72ef86dbf2cf46c5e66ecd04ae88..4c229b5e8f6f78162b08b0a9eb8c1cc6dfc4b293 100644
--- a/prelude/hashset.v
+++ b/prelude/hashset.v
@@ -3,8 +3,8 @@
 (** This file implements finite set using hash maps. Hash sets are represented
 using radix-2 search trees. Each hash bucket is thus indexed using an binary
 integer of type [Z], and contains an unordered list without duplicates. *)
-From prelude Require Export fin_maps listset.
-From prelude Require Import zmap.
+From iris.prelude Require Export fin_maps listset.
+From iris.prelude Require Import zmap.
 
 Record hashset {A} (hash : A → Z) := Hashset {
   hashset_car : Zmap (list A);
diff --git a/prelude/lexico.v b/prelude/lexico.v
index 43ecf2cdfef5ce020c264d22cecafbbce1c3e40e..48880234ddb18229a8de46a003a14c9849e4c9c6 100644
--- a/prelude/lexico.v
+++ b/prelude/lexico.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This files defines a lexicographic order on various common data structures
 and proves that it is a partial order having a strong variant of trichotomy. *)
-From prelude Require Import numbers.
+From iris.prelude Require Import numbers.
 
 Notation cast_trichotomy T :=
   match T with
diff --git a/prelude/list.v b/prelude/list.v
index 7359498536696a1eaadfd817f78d5c6c4bd19664..ef4d127b569951e33b5d30d151c00569a56ef8ad 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -3,7 +3,7 @@
 (** This file collects general purpose definitions and theorems on lists that
 are not in the Coq standard library. *)
 From Coq Require Export Permutation.
-From prelude Require Export numbers base option.
+From iris.prelude Require Export numbers base option.
 
 Arguments length {_} _.
 Arguments cons {_} _ _.
diff --git a/prelude/listset.v b/prelude/listset.v
index fb8e8145b8b810a670e5adbfe3943fd29c1316fe..0f8cfe42af13eefe8b1b12f12c5313d66bb175f5 100644
--- a/prelude/listset.v
+++ b/prelude/listset.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
-From prelude Require Export collections list.
+From iris.prelude Require Export collections list.
 
 Record listset A := Listset { listset_car: list A }.
 Arguments listset_car {_} _.
diff --git a/prelude/listset_nodup.v b/prelude/listset_nodup.v
index 40ee72baa966d42be08f4afb2b042c7e0b0fc833..aaa008843ed19d1f3d9a27990fddd118a3e46db2 100644
--- a/prelude/listset_nodup.v
+++ b/prelude/listset_nodup.v
@@ -3,7 +3,7 @@
 (** This file implements finite as unordered lists without duplicates.
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
-From prelude Require Export collections list.
+From iris.prelude Require Export collections list.
 
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
diff --git a/prelude/mapset.v b/prelude/mapset.v
index 5667851ed2739ad6b8cbc021b6c5f24e13c2a605..e8d5407b83fad5df2d014325794511c92e0b4511 100644
--- a/prelude/mapset.v
+++ b/prelude/mapset.v
@@ -3,7 +3,7 @@
 (** This files gives an implementation of finite sets using finite maps with
 elements of the unit type. Since maps enjoy extensional equality, the
 constructed finite sets do so as well. *)
-From prelude Require Export fin_map_dom.
+From iris.prelude Require Export fin_map_dom.
 
 Record mapset (M : Type → Type) : Type :=
   Mapset { mapset_car: M (unit : Type) }.
diff --git a/prelude/natmap.v b/prelude/natmap.v
index 253c2d44bd4f3b5303ba0d3b155523aaf9f55b8d..5845901a62cf9d3fe2fc6b63806409e5c1e86b05 100644
--- a/prelude/natmap.v
+++ b/prelude/natmap.v
@@ -3,7 +3,7 @@
 (** This files implements a type [natmap A] of finite maps whose keys range
 over Coq's data type of unary natural numbers [nat]. The implementation equips
 a list with a proof of canonicity. *)
-From prelude Require Import fin_maps mapset.
+From iris.prelude Require Import fin_maps mapset.
 
 Notation natmap_raw A := (list (option A)).
 Definition natmap_wf {A} (l : natmap_raw A) :=
diff --git a/prelude/nmap.v b/prelude/nmap.v
index 630a5c28a2f7b4f07a294e6a0110518cd270be83..11fead13c53c361d4e852924c79a4aae2e08f425 100644
--- a/prelude/nmap.v
+++ b/prelude/nmap.v
@@ -2,8 +2,8 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This files extends the implementation of finite over [positive] to finite
 maps whose keys range over Coq's data type of binary naturals [N]. *)
-From prelude Require Import pmap mapset.
-From prelude Require Export prelude fin_maps.
+From iris.prelude Require Import pmap mapset.
+From iris.prelude Require Export prelude fin_maps.
 
 Local Open Scope N_scope.
 
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 2daa380b7e1d7c58a5494cafe4ab69847f26abf2..50d60a0da3e354f8eda5e9190c496d5d126f15eb 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -5,7 +5,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
 From Coq Require Export Eqdep PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
-From prelude Require Export base decidable option.
+From iris.prelude Require Export base decidable option.
 Open Scope nat_scope.
 
 Coercion Z.of_nat : nat >-> Z.
diff --git a/prelude/option.v b/prelude/option.v
index 90d7bc3ec484d87cc8db49761eae1d4203cb8b19..2155d932ed484de68c436347629131eba4398a4d 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
-From prelude Require Export tactics.
+From iris.prelude Require Export tactics.
 
 Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
   | ReflectSome x : P x → option_reflect P Q (Some x)
diff --git a/prelude/orders.v b/prelude/orders.v
index 93f0717b2f0ddd4b779ebfd811407e5a7066a76b..e7a9abbfd5013905aa71cdac48d19e2b54826085 100644
--- a/prelude/orders.v
+++ b/prelude/orders.v
@@ -3,7 +3,7 @@
 (** This file collects common properties of pre-orders and semi lattices. This
 theory will mainly be used for the theory on collections and finite maps. *)
 From Coq Require Export Sorted.
-From prelude Require Export tactics list.
+From iris.prelude Require Export tactics list.
 
 (** * Arbitrary pre-, parial and total orders *)
 (** Properties about arbitrary pre-, partial, and total orders. We do not use
diff --git a/prelude/pmap.v b/prelude/pmap.v
index e18113c4778e1c5dd3454ff8ffedd80e4931d1db..483eac8b16690b182496e9510a4b4bb44acd2709 100644
--- a/prelude/pmap.v
+++ b/prelude/pmap.v
@@ -8,8 +8,8 @@ However, we extend Leroy's implementation by packing the trees into a Sigma
 type such that canonicity of representation is ensured. This is necesarry for
 Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
-From prelude Require Import mapset.
-From prelude Require Export fin_maps.
+From iris.prelude Require Import mapset.
+From iris.prelude Require Export fin_maps.
 
 Local Open Scope positive_scope.
 Local Hint Extern 0 (@eq positive _ _) => congruence.
diff --git a/prelude/prelude.v b/prelude/prelude.v
index ad1f1cb45ae0dd931b16062b51e216ae90742f49..a1cf5343c8d2d6938df992aa0f2e533cce261695 100644
--- a/prelude/prelude.v
+++ b/prelude/prelude.v
@@ -1,6 +1,6 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From prelude Require Export
+From iris.prelude Require Export
   base
   tactics
   orders
diff --git a/prelude/pretty.v b/prelude/pretty.v
index 61e4a449b502ca598652a54ce4ba152b69ed2c86..7637aedf0ec050d3b7d4ce6fbbcc07cfafd96625 100644
--- a/prelude/pretty.v
+++ b/prelude/pretty.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From prelude Require Export strings.
-From prelude Require Import relations.
+From iris.prelude Require Export strings.
+From iris.prelude Require Import relations.
 From Coq Require Import Ascii.
 
 Class Pretty A := pretty : A → string.
diff --git a/prelude/proof_irrel.v b/prelude/proof_irrel.v
index 381a8a91f93b06cd62122aa49b95ac66a160fd8c..4afb6c5d13258b604db923c01217d47097853dbe 100644
--- a/prelude/proof_irrel.v
+++ b/prelude/proof_irrel.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects facts on proof irrelevant types/propositions. *)
 From Coq Require Import Eqdep_dec.
-From prelude Require Export base.
+From iris.prelude Require Export base.
 
 Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
 
diff --git a/prelude/relations.v b/prelude/relations.v
index 55f33d86e74e4f376c560f181e368b2530e4823a..e5a5436c0781f56d8900547b3dac8695d9ea0afa 100644
--- a/prelude/relations.v
+++ b/prelude/relations.v
@@ -5,7 +5,7 @@ These are particularly useful as we define the operational semantics as a
 small step semantics. This file defines a hint database [ars] containing
 some theorems on abstract rewriting systems. *)
 From Coq Require Import Wf_nat.
-From prelude Require Export tactics base.
+From iris.prelude Require Export tactics base.
 
 (** * Definitions *)
 Section definitions.
diff --git a/prelude/sets.v b/prelude/sets.v
index dbb25e14ac0a6e646458bf255ddba6a1e7bbcdc9..0a96963fbaebfb9f535d7c8823102194c433a5f3 100644
--- a/prelude/sets.v
+++ b/prelude/sets.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements sets as functions into Prop. *)
-From prelude Require Export collections.
+From iris.prelude Require Export collections.
 
 Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
 Add Printing Constructor set.
diff --git a/prelude/streams.v b/prelude/streams.v
index 114b5c79aaf317866ad5d506b827cc700f814a39..130510c016ce0b781988ab64d2405dc46423f6da 100644
--- a/prelude/streams.v
+++ b/prelude/streams.v
@@ -1,6 +1,6 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From prelude Require Export tactics.
+From iris.prelude Require Export tactics.
 
 CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
 Arguments scons {_} _ _.
diff --git a/prelude/stringmap.v b/prelude/stringmap.v
index 56f2ece6a88242052ad3165084f5fa7a76ca642e..f6eedf071bd0b76e3488edc763e0824e41a571f1 100644
--- a/prelude/stringmap.v
+++ b/prelude/stringmap.v
@@ -4,8 +4,8 @@
 range over Coq's data type of strings [string]. The implementation uses radix-2
 search trees (uncompressed Patricia trees) as implemented in the file [pmap]
 and guarantees logarithmic-time operations. *)
-From prelude Require Export fin_maps pretty.
-From prelude Require Import gmap.
+From iris.prelude Require Export fin_maps pretty.
+From iris.prelude Require Import gmap.
 
 Notation stringmap := (gmap string).
 Notation stringset := (gset string).
diff --git a/prelude/strings.v b/prelude/strings.v
index f0f7e991ffebb4353eb47c31295d57594eacd619..3d5cfac7c02afe181a2dd69f1f4ebe4f37153d53 100644
--- a/prelude/strings.v
+++ b/prelude/strings.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 From Coq Require Import Ascii.
 From Coq Require Export String.
-From prelude Require Export countable.
+From iris.prelude Require Export countable.
 
 (** * Fix scopes *)
 Open Scope string_scope.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 7f6f1f1b2456eadcb2915b4b400e14d227bf5b4a..970982061a39cc8707303d2cc27ffd1069ee18bd 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -4,7 +4,7 @@
 the development. *)
 From Coq Require Import Omega.
 From Coq Require Export Psatz.
-From prelude Require Export decidable.
+From iris.prelude Require Export decidable.
 
 Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
 Proof. intros ->; reflexivity. Qed.
diff --git a/prelude/vector.v b/prelude/vector.v
index a9e4bcff137c1aae9d52dbd5d751af711126b68f..ee6e9b1fd6a1e50f8514416c42563a2fe799b47f 100644
--- a/prelude/vector.v
+++ b/prelude/vector.v
@@ -5,7 +5,7 @@
 definitions from the standard library, but renames or changes their notations,
 so that it becomes more consistent with the naming conventions in this
 development. *)
-From prelude Require Import list finite.
+From iris.prelude Require Import list finite.
 Open Scope vector_scope.
 
 (** * The fin type *)
diff --git a/prelude/zmap.v b/prelude/zmap.v
index c80d7f71051ddf6a51c1974c11e017010973d439..238fadc46c63d485cb2a4077ff7a1acfcd34fe18 100644
--- a/prelude/zmap.v
+++ b/prelude/zmap.v
@@ -2,8 +2,8 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This files extends the implementation of finite over [positive] to finite
 maps whose keys range over Coq's data type of binary naturals [Z]. *)
-From prelude Require Import pmap mapset.
-From prelude Require Export prelude fin_maps.
+From iris.prelude Require Import pmap mapset.
+From iris.prelude Require Export prelude fin_maps.
 Local Open Scope Z_scope.
 
 Record Zmap (A : Type) : Type :=
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 55090ec664ac1e21f1dc0ff3ce0e2f3afb9b11b1..7cdfcea5b93afe1852e92b3f0fff193bf4cd2dc2 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,5 +1,5 @@
-From program_logic Require Export hoare.
-From program_logic Require Import wsat ownership.
+From iris.program_logic Require Export hoare.
+From iris.program_logic Require Import wsat ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || set_solver.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 792dced38bf8b2df94988604c0a45de759116c28..5189460abfe1acc2717fa4f623e71ed7d86da89e 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,5 +1,5 @@
-From algebra Require Export auth upred_tactics.
-From program_logic Require Export invariants ghost_ownership.
+From iris.algebra Require Export auth upred_tactics.
+From iris.program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 96c6cd962bff668eaa7ffab0ac4f76a75038163d..d5ddff47fb24e75815376a4e4b920e51b8217fad 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -1,7 +1,7 @@
-From prelude Require Export functions.
-From algebra Require Export iprod.
-From program_logic Require Export pviewshifts global_functor.
-From program_logic Require Import ownership.
+From iris.prelude Require Export functions.
+From iris.algebra Require Export iprod.
+From iris.program_logic Require Export pviewshifts global_functor.
+From iris.program_logic Require Import ownership.
 Import uPred.
 
 Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index fc74301a7d0d8e4bea16d543fed1f2b0065bec47..79acdffdb354ccbc6851cc7b469c5702cd6e7bb9 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -1,5 +1,5 @@
-From algebra Require Export iprod.
-From program_logic Require Export model.
+From iris.algebra Require Export iprod.
+From iris.program_logic Require Export model.
 
 (** Index of a CMRA in the product of global CMRAs. *)
 Definition gid := nat.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 2d9ae68961c3792bfce79eb79ed66b3eb9879523..b89becfd19414838c96454f3d4490bb4a6335ad2 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,4 +1,4 @@
-From program_logic Require Export weakestpre viewshifts.
+From iris.program_logic Require Export weakestpre viewshifts.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
     (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ :=
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index d14528599c2e43541b7870562617b07ca8a5cf10..a054226babfdbe12ba899396a4d8297e9e4313c3 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -1,6 +1,6 @@
-From algebra Require Import upred_tactics.
-From program_logic Require Export hoare lifting.
-From program_logic Require Import ownership.
+From iris.algebra Require Import upred_tactics.
+From iris.program_logic Require Export hoare lifting.
+From iris.program_logic Require Import ownership.
 Import uPred.
 
 Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 05388245b9c8324937db307598d1761c461ad7e8..86d68258839e438455cd3391eb8f8024295b62d3 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -1,6 +1,6 @@
-From algebra Require Export base.
-From program_logic Require Import ownership.
-From program_logic Require Export namespaces pviewshifts weakestpre.
+From iris.algebra Require Export base.
+From iris.program_logic Require Import ownership.
+From iris.program_logic Require Export namespaces pviewshifts weakestpre.
 Import uPred.
 Local Hint Extern 100 (@eq coPset _ _) => set_solver.
 Local Hint Extern 100 (@subseteq coPset _ _) => set_solver.
@@ -57,7 +57,7 @@ Qed.
 Lemma pvs_open_close E N P Q R :
   nclose N ⊆ E →
   R ⊑ inv N P →
-  R ⊑ (▷ P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷ P ★ Q)) →
+  R ⊑ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
   R ⊑ (|={E}=> Q).
 Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
 
@@ -68,8 +68,8 @@ Lemma wp_open_close E e N P Φ R :
   R ⊑ #> e @ E {{ Φ }}.
 Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
 
-Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊑ pvs E E (inv N P).
-Proof. 
+Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊑ |={E}=> inv N P.
+Proof.
   intros. rewrite -(pvs_mask_weaken N) //.
   by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
 Qed.
diff --git a/program_logic/language.v b/program_logic/language.v
index 57a4859ba9ec01fe84cfc412131119785f7c4822..520d61aeebf350e390ac94a74b68358fe66cabdf 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -1,4 +1,4 @@
-From algebra Require Export cofe.
+From iris.algebra Require Export cofe.
 
 Structure language := Language {
   expr : Type;
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 957ecbfa9acefe2db838a4310e0cc798b97eb411..425c10f4e57968dedef5ffe48d36d39947cd6c99 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
-From program_logic Require Export weakestpre.
-From program_logic Require Import wsat ownership.
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import wsat ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => set_solver.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/program_logic/model.v b/program_logic/model.v
index 97ceebf4a23a0332f208744a7dbcdc6e3d192531..ce2cf3f1b62ad2a9ac3bec02ac7447fc20f4f0ed 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,6 +1,6 @@
-From algebra Require Export upred.
-From program_logic Require Export resources.
-From algebra Require Import cofe_solver.
+From iris.algebra Require Export upred.
+From iris.program_logic Require Export resources.
+From iris.algebra Require Import cofe_solver.
 
 (* The Iris program logic is parametrized by a locally contractive functor
 from the category of COFEs to the category of CMRAs, which is instantiated
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index e6bb7e1923102f732cec1678e067d5e5964f725c..3c7ba893291fc8b40b712e89d82b4b482680b5a3 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -1,5 +1,5 @@
-From prelude Require Export countable co_pset.
-From algebra Require Export base.
+From iris.prelude Require Export countable co_pset.
+From iris.algebra Require Export base.
 
 Definition namespace := list positive.
 Definition nroot : namespace := nil.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 39104384418c89ae8068b12e461ad997e90b3fcc..1a6474d475be2f8dac7506de95d740cd9768495b 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -1,4 +1,4 @@
-From program_logic Require Export model.
+From iris.program_logic Require Export model.
 
 Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
   uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index e98fa4095f84f1ac391908def6bf2915fa5a5f76..ed0900943c5768d852684bad25db9da3a2b8257c 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,6 +1,6 @@
-From prelude Require Export co_pset.
-From program_logic Require Export model.
-From program_logic Require Import ownership wsat.
+From iris.prelude Require Export co_pset.
+From iris.program_logic Require Export model.
+From iris.program_logic Require Import ownership wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => set_solver.
 Local Hint Extern 100 (_ ∉ _) => set_solver.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index cab118fd67418a6c12090083d02b17a3d8ce8265..d703b28a14a1075ee0af235c8700ec1d8e263f68 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -1,6 +1,6 @@
-From algebra Require Export fin_maps agree excl.
-From algebra Require Import upred.
-From program_logic Require Export language.
+From iris.algebra Require Export fin_maps agree excl.
+From iris.algebra Require Import upred.
+From iris.program_logic Require Export language.
 
 Record res (Λ : language) (A : cofeT) (M : cmraT) := Res {
   wld : mapR positive (agreeR A);
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 5e41b83a7cecced7a7b684b8672a6108237cfdf3..22cecf668e26fb65ce41d9f7ba6b86de1448b500 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -1,5 +1,5 @@
-From algebra Require Export agree.
-From program_logic Require Export ghost_ownership.
+From iris.algebra Require Export agree.
+From iris.program_logic Require Export ghost_ownership.
 Import uPred.
 
 Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
diff --git a/program_logic/sts.v b/program_logic/sts.v
index e9034fb736251ef39b68fc3b5b2f063ea3af297b..76a00f4228c2c1968cef2e97bc762893f63ac2e6 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,5 +1,5 @@
-From algebra Require Export sts upred_tactics.
-From program_logic Require Export invariants ghost_ownership.
+From iris.algebra Require Export sts upred_tactics.
+From iris.program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
 (** The CMRA we need. *)
diff --git a/program_logic/tactics.v b/program_logic/tactics.v
index f3e1b6e3df99086607d907bf025da59569f8f3a0..2ac6a67cd56086e44958c84e785001a7a34f80a4 100644
--- a/program_logic/tactics.v
+++ b/program_logic/tactics.v
@@ -1,5 +1,5 @@
-From algebra Require Export upred_tactics.
-From program_logic Require Export pviewshifts.
+From iris.algebra Require Export upred_tactics.
+From iris.program_logic Require Export pviewshifts.
 Import uPred.
 
 Module uPred_reflection_pvs.
diff --git a/program_logic/tests.v b/program_logic/tests.v
index 0a5ca9fdbd04b28b8ab8a43915b3cd6e4ae5cc38..f9f66bfd748528b32b98193ecb2553a7b53fd01e 100644
--- a/program_logic/tests.v
+++ b/program_logic/tests.v
@@ -1,5 +1,5 @@
 (** This file tests a bunch of things. *)
-From program_logic Require Import model saved_prop.
+From iris.program_logic Require Import model saved_prop.
 
 Module ModelTest. (* Make sure we got the notations right. *)
   Definition iResTest {Λ : language} {Σ : iFunctor}
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 417833660a3c3ea05633026378ea0b5716c9a477..4ac9228ac0f103a49f1a785d0a4d4bc679c100e2 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,5 +1,5 @@
-From program_logic Require Import ownership.
-From program_logic Require Export pviewshifts invariants ghost_ownership.
+From iris.program_logic Require Import ownership.
+From iris.program_logic Require Export pviewshifts invariants ghost_ownership.
 Import uPred.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 25e8c2a8ea5bbebd8c0bb224250a75a6e0ca247f..a0244cdb48d7bb7da99ec1930df723444fc5a493 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,5 @@
-From program_logic Require Export pviewshifts.
-From program_logic Require Import wsat.
+From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Import wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || set_solver.
 Local Hint Extern 100 (_ ∉ _) => set_solver.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 5cbcab7119b464bed59853a034a75c0b371535b1..7eee60b1e02242539154eb33bbf0c2118d7e6e5e 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -1,6 +1,6 @@
-From prelude Require Export co_pset.
-From program_logic Require Export model.
-From algebra Require Export cmra_big_op cmra_tactics.
+From iris.prelude Require Export co_pset.
+From iris.program_logic Require Export model.
+From iris.algebra Require Export cmra_big_op cmra_tactics.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 10 (✓{_} _) => solve_validN.
 Local Hint Extern 1 (✓{_} gst _) => apply gst_validN.