Put the internal namespace definitions of the lifetime logic in the model.

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  *)

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