diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 2ea42a57a9fb5f9a38061ede335f4586cc885890..79029f48e4b9a8e42f8c6d5d80a0f68906595959 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,13 +1,12 @@
 From iris.base_logic Require Export derived.
 
-Module uPred.
-  Include uPred_entails.
-  Include uPred_primitive.
-  Include uPred_derived.
+Module Import uPred.
+  Export upred.uPred.
+  Export primitive.uPred.
+  Export derived.uPred.
 End uPred.
 
 (* Hint DB for the logic *)
-Import uPred.
 Hint Resolve pure_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 7361ad14752e70666af09eaad19906a3e2a13897..80f7d2e175a13de4f60b7c4423b80cb5b9a395f5 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export primitive.
-Import uPred_entails uPred_primitive.
+Import upred.uPred primitive.uPred.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
 Instance: Params (@uPred_iff) 1.
@@ -34,7 +34,7 @@ Arguments timelessP {_} _ {_}.
 Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
 Arguments persistentP {_} _ {_}.
 
-Module uPred_derived.
+Module uPred.
 Section derived.
 Context {M : ucmraT}.
 Implicit Types φ : Prop.
@@ -858,5 +858,4 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
 Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 End derived.
-
-End uPred_derived.
+End uPred.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 566343342a23d42549d3b8c4161385ae54d83d24..7a31c8d93da90d3c014ea410f05bec5fd677eab9 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -1,5 +1,4 @@
 From iris.base_logic Require Import base_logic.
-Import upred.
 
 (* In this file we show that the bupd can be thought of a kind of
    step-indexed double-negation when our meta-logic is classical *)
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index cce3c8057cab7271dfe4d73f59ecfda721086cf5..49a856103799092a32ce4b34c6c9774905bb9e19 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -40,7 +40,7 @@ Section fractional.
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
     PersistentP P → Fractional (λ _, P).
-  Proof. intros HP q q'. by apply uPred_derived.always_sep_dup. Qed.
+  Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 85dfdb49ea08d8c48d3300a5a6e9090acf0caaa1..0a6c7239e5a53e0c0764d6864b77b84efaafedcb 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -192,7 +192,7 @@ Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
 Notation "P -∗ Q" := (P ⊢ Q)
   (at level 99, Q at level 200, right associativity) : C_scope.
 
-Module uPred_primitive.
+Module uPred.
 Definition unseal :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
   uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
@@ -596,4 +596,4 @@ Proof. by unseal. Qed.
 Lemma cofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 End primitive.
-End uPred_primitive.
+End uPred.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index 501d8f1a2f0f106edefa8319acb784e7b96be3eb..b2c7d8abf2e851601c7cda8d7ab1a61c1f1fb836 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -1,5 +1,5 @@
-From iris.base_logic Require Export primitive derived.
-Import uPred_entails uPred_primitive.
+From iris.base_logic Require Export base_logic.
+Import uPred.
 
 Section adequacy.
 Context {M : ucmraT}.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index ac98bdddc617447ec8de647344cce6372a077ca4..cb12bf33d8323527bfe7080a2c781996b03ab117 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -138,7 +138,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
   (at level 95, no associativity) : C_scope.
 Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
 
-Module uPred_entails.
+Module uPred.
 Section entails.
 Context {M : ucmraT}.
 Implicit Types P Q : uPred M.
@@ -173,4 +173,4 @@ Proof. by intros ->. Qed.
 Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
 Proof. by intros ? <-. Qed.
 End entails.
-End uPred_entails.
+End uPred.