Tweak.

theories/lifetime.v

@@ -47,15 +47,15 @@ Section defs.
   Definition idx_borrow_own (q : Qp) (i : borrow_idx) :=
     own borrow_tok_name (◯ {[ i := q ]}).
 
-End defs.
+  Parameter idx_borrow:
+    ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
 
-Typeclasses Opaque lft_own lft_dead .
+  Definition borrow (κ : lifetime) (P : iProp Σ) : iProp Σ :=
+    (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
 
-Parameter idx_borrow:
-  ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
+End defs.
 
-Definition borrow `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ) : iProp Σ :=
-  (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
+Typeclasses Opaque lft_own lft_dead borrow.
 
 (*** Notations  *)