diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index d208f940ee24ea8c517faeaca36deb093d88d344..2c60ff7459d0f8a73df266fc21adc6a117d79720 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From gpfsl.logic Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 From iris.prelude Require Import options.
 
-Definition na_bor `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
+Definition na_bor {View} `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : monPred _ _) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
+  Context {View} `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
           (tid : na_inv_pool_name) (N : namespace).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).