diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 22f12192c9d38d48c101d9ca345effa079700d76..f2dd298f45b928fbb2a14cbc6214cadbb7cc77ac 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -5,9 +5,6 @@ From iris.base_logic.lib Require Import boxes fractional.
 Set Default Proof Using "Type".
 
 Definition lftN : namespace := nroot .@ "lft".
-Definition borN : namespace := lftN .@ "bor".
-Definition inhN : namespace := lftN .@ "inh".
-Definition mgmtN : namespace := lftN .@ "mgmt".
 
 Module Type lifetime_sig.
   (** CMRAs needed by the lifetime logic  *)
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 7ee2738816323458d685fedf126842a133d8fe6d..7f286d7a9fa12aacc86e85680eb88a815fac89fc 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -6,6 +6,10 @@ From lrust.lifetime Require Export lifetime_sig.
 Set Default Proof Using "Type".
 Import uPred.
 
+Definition borN : namespace := lftN .@ "bor".
+Definition inhN : namespace := lftN .@ "inh".
+Definition mgmtN : namespace := lftN .@ "mgmt".
+
 Definition atomic_lft := positive.
 (* HACK : We need to make sure this is not in the top-level context,
    so that it does not conflict with the *definition* of [lft] that we