test performance without typeclasses opaque

theories/lifetime/definitions.v

@@ -200,9 +200,10 @@ Notation "&{ κ , i } P" := (idx_bor κ i P)
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 
-Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
+Typeclasses Opaque lft_inv_alive lft_vs_inv lft_vs lft_incl.
+(*Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
-  idx_bor_own idx_bor raw_bor bor.
+  idx_bor_own idx_bor raw_bor bor.*)
 
 Section basic_properties.
 Context `{invG Σ, lftG Σ}.

theories/lifetime/primitive.v

@@ -393,7 +393,9 @@ Lemma lft_inh_extend E κ P Q :
      (∀ Q', ▷ lft_inh κ true Q' ={E}=∗ ∃ Q'',
             ▷ ▷ (Q' ≡ (P ∗ Q'')) ∗ ▷ P ∗ ▷ lft_inh κ true Q'').
 Proof.
-  rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
+  iIntros (?) "H".
+  Set Typeclasses Debug.
+  unfold lft_inh. iDestruct "H" as (PE) "[>HE Hbox]".
   iMod (slice_insert_empty _ _ true _ P with "Hbox")
     as (γE) "(% & #Hslice & Hbox)".
   iMod (own_inh_update with "HE") as "[HE HE◯]".