From 942161994c060c6776dcf305535a8c13cc53595d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 10 Mar 2016 12:01:08 +0100
Subject: [PATCH] Give the project a top-level name so it can be make
 installed.

Thanks to Amin Timany for the suggestion.
---
 _CoqProject                     |  2 +-
 algebra/agree.v                 |  4 ++--
 algebra/auth.v                  |  4 ++--
 algebra/base.v                  |  2 +-
 algebra/cmra.v                  |  2 +-
 algebra/cmra_big_op.v           |  4 ++--
 algebra/cmra_tactics.v          |  4 ++--
 algebra/cofe.v                  |  2 +-
 algebra/cofe_solver.v           |  2 +-
 algebra/dec_agree.v             |  2 +-
 algebra/dra.v                   |  2 +-
 algebra/excl.v                  |  4 ++--
 algebra/fin_maps.v              |  6 +++---
 algebra/frac.v                  |  4 ++--
 algebra/iprod.v                 |  4 ++--
 algebra/option.v                |  4 ++--
 algebra/sts.v                   |  6 +++---
 algebra/upred.v                 |  2 +-
 algebra/upred_big_op.v          |  4 ++--
 algebra/upred_tactics.v         |  4 ++--
 barrier/barrier.v               |  2 +-
 barrier/client.v                |  6 +++---
 barrier/proof.v                 | 12 ++++++------
 barrier/protocol.v              |  4 ++--
 barrier/specification.v         |  6 +++---
 heap_lang/derived.v             |  2 +-
 heap_lang/heap.v                |  8 ++++----
 heap_lang/lang.v                |  6 +++---
 heap_lang/lifting.v             | 10 +++++-----
 heap_lang/notation.v            |  2 +-
 heap_lang/par.v                 |  4 ++--
 heap_lang/spawn.v               |  6 +++---
 heap_lang/substitution.v        |  2 +-
 heap_lang/tactics.v             |  4 ++--
 heap_lang/tests.v               |  4 ++--
 heap_lang/wp_tactics.v          |  4 ++--
 prelude/bsets.v                 |  2 +-
 prelude/co_pset.v               |  4 ++--
 prelude/collections.v           |  2 +-
 prelude/countable.v             |  2 +-
 prelude/decidable.v             |  2 +-
 prelude/error.v                 |  2 +-
 prelude/fin_collections.v       |  4 ++--
 prelude/fin_map_dom.v           |  2 +-
 prelude/fin_maps.v              |  2 +-
 prelude/finite.v                |  2 +-
 prelude/functions.v             |  2 +-
 prelude/gmap.v                  |  4 ++--
 prelude/hashset.v               |  4 ++--
 prelude/lexico.v                |  2 +-
 prelude/list.v                  |  2 +-
 prelude/listset.v               |  2 +-
 prelude/listset_nodup.v         |  2 +-
 prelude/mapset.v                |  2 +-
 prelude/natmap.v                |  2 +-
 prelude/nmap.v                  |  4 ++--
 prelude/numbers.v               |  2 +-
 prelude/option.v                |  2 +-
 prelude/orders.v                |  2 +-
 prelude/pmap.v                  |  4 ++--
 prelude/prelude.v               |  2 +-
 prelude/pretty.v                |  4 ++--
 prelude/proof_irrel.v           |  2 +-
 prelude/relations.v             |  2 +-
 prelude/sets.v                  |  2 +-
 prelude/streams.v               |  2 +-
 prelude/stringmap.v             |  4 ++--
 prelude/strings.v               |  2 +-
 prelude/tactics.v               |  2 +-
 prelude/vector.v                |  2 +-
 prelude/zmap.v                  |  4 ++--
 program_logic/adequacy.v        |  4 ++--
 program_logic/auth.v            |  4 ++--
 program_logic/ghost_ownership.v |  8 ++++----
 program_logic/global_functor.v  |  4 ++--
 program_logic/hoare.v           |  2 +-
 program_logic/hoare_lifting.v   |  6 +++---
 program_logic/invariants.v      | 12 ++++++------
 program_logic/language.v        |  2 +-
 program_logic/lifting.v         |  4 ++--
 program_logic/model.v           |  6 +++---
 program_logic/namespaces.v      |  4 ++--
 program_logic/ownership.v       |  2 +-
 program_logic/pviewshifts.v     |  6 +++---
 program_logic/resources.v       |  6 +++---
 program_logic/saved_prop.v      |  4 ++--
 program_logic/sts.v             |  4 ++--
 program_logic/tactics.v         |  4 ++--
 program_logic/tests.v           |  2 +-
 program_logic/viewshifts.v      |  4 ++--
 program_logic/weakestpre.v      |  4 ++--
 program_logic/wsat.v            |  6 +++---
 92 files changed, 168 insertions(+), 168 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index c179fb492..aedb367b8 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 4039c7e40..cab28bc94 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 f34174292..e2e54fb18 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 5235048e2..483d63d72 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 8725d9665..08256da86 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 3094846ea..2e3d894e6 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 342c0ba85..6943f64bf 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 b1bf31032..0e880514d 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 855db70a1..280dce025 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 202b80ffa..b7c37089a 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 1909b430a..36fe74bb7 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 884c01a02..9f731370e 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 28fa2fe7a..0215ded50 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 e2e609f7c..daf952db3 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 abf208ab5..34f4dcac5 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 ba5b87fea..1530ecd6e 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 5a1fc8bd6..216f7bd0e 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 306906368..968d89add 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 b8ac2cd8f..d9e700cb3 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 b8c9368bc..5fc479b60 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 d9dd2b4e6..d8e4a6618 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 57465a50d..c630e7da0 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 ac18c35cf..40b99c0ad 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 53b315536..4294c9e32 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 8de9c66e3..2f57dc41d 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 4760925d5..327bb7cc4 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 4ca6c7dd3..7f31f37b5 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 bc135938a..3d63e057b 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 0e0edce3f..5df7f53b5 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 7ac1a85e7..200cccb7d 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 b3b9d1f9d..f65ac187f 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 c26c69590..e3db4ef0e 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 7f854cbb4..5ecd40c6b 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 441e59614..1fea861c4 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 95ddc3f1b..ce5d9c930 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 9a4fc6253..8d438899a 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 40216c1a3..f0da19b35 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 d2feb8203..80a750697 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 13bba4fea..ed72cdd0c 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 4db318974..6267748cf 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 d57c025c5..4dfd94a37 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 bed968e6c..cba021739 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 65850cbf1..5fafe28d5 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 0d735863b..62b356ab4 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 81ad3e2c0..ba5dab026 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 4075de942..02a0f84a5 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 4842faa62..1ae5080e7 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 c062478e4..d59577320 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 e5779a2fd..4c229b5e8 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 43ecf2cdf..48880234d 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 735949853..ef4d127b5 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 fb8e8145b..0f8cfe42a 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 40ee72baa..aaa008843 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 5667851ed..e8d5407b8 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 253c2d44b..5845901a6 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 630a5c28a..11fead13c 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 2daa380b7..50d60a0da 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 90d7bc3ec..2155d932e 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 93f0717b2..e7a9abbfd 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 e18113c47..483eac8b1 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 ad1f1cb45..a1cf5343c 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 61e4a449b..7637aedf0 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 381a8a91f..4afb6c5d1 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 55f33d86e..e5a5436c0 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 dbb25e14a..0a96963fb 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 114b5c79a..130510c01 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 56f2ece6a..f6eedf071 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 f0f7e991f..3d5cfac7c 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 7f6f1f1b2..970982061 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 a9e4bcff1..ee6e9b1fd 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 c80d7f710..238fadc46 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 55090ec66..7cdfcea5b 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 792dced38..5189460ab 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 96c6cd962..d5ddff47f 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 fc74301a7..79acdffdb 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 2d9ae6896..b89becfd1 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 d14528599..a054226ba 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 05388245b..86d682588 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 57a4859ba..520d61aee 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 957ecbfa9..425c10f4e 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 97ceebf4a..ce2cf3f1b 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 e6bb7e192..3c7ba8932 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 391043844..1a6474d47 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 e98fa4095..ed0900943 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 cab118fd6..d703b28a1 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 5e41b83a7..22cecf668 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 e9034fb73..76a00f422 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 f3e1b6e3d..2ac6a67cd 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 0a5ca9fdb..f9f66bfd7 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 417833660..4ac9228ac 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 25e8c2a8e..a0244cdb4 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 5cbcab711..7eee60b1e 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.
-- 
GitLab