From c34388eaf16cb62f68c9593a61349f6c53b876f8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 4 Jan 2017 11:43:36 +0100
Subject: [PATCH] test performance without typeclasses opaque
---
theories/lifetime/definitions.v | 5 +++--
theories/lifetime/primitive.v | 4 +++-
2 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index d98f4dd1..01d78a70 100644
--- a/theories/lifetime/definitions.v
+++ b/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 Σ}.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 235510a1..8bcdcbd2 100644
--- a/theories/lifetime/primitive.v
+++ b/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◯]".
--
GitLab