fix na_borrow

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