From fa725d2e4f45fcbef8fb5a13a29eebe55338d5bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Jun 2023 17:40:42 +0200
Subject: [PATCH] Do not make sealed definitions TC opaque.

---
 theories/lang/heap.v                | 5 ++---
 theories/lifetime/model/primitive.v | 8 ++++----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index c147dede..ba10b34f 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -66,7 +66,7 @@ Section definitions.
          ∗ ⌜heap_freeable_rel σ hF⌝)%I.
 End definitions.
 
-Global Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
+Global Typeclasses Opaque heap_mapsto_vec.
 Global Instance: Params (@heap_mapsto) 4 := {}.
 Global Instance: Params (@heap_freeable) 5 := {}.
 
@@ -127,8 +127,7 @@ Section heap.
   Global Instance frame_mapsto p l v q1 q2 q :
     FrameFractionalQp q1 q2 q →
     Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
-  (* FIXME: somehow Φ gets inferred wrong here. *)
-  Proof. apply: (frame_fractional _ _ _ (λ q, l ↦{q} v)%I). Qed.
+  Proof. apply: frame_fractional. Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index edbf4174..cf2e327f 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -322,8 +322,8 @@ Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
 Proof. split; first done. apply _. Qed.
 Global Instance frame_lft_tok p κ q1 q2 q :
-    FrameFractionalQp q1 q2 q →
-    Frame p q1.[κ] q2.[κ] q.[κ] | 5.
+  FrameFractionalQp q1 q2 q →
+  Frame p q1.[κ] q2.[κ] q.[κ] | 5.
 (* FIXME: somehow Φ gets inferred wrong here. *)
 Proof. apply: (frame_fractional _ _ _ (λ q, q.[κ])%I). Qed.
 
@@ -336,8 +336,8 @@ Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
 Proof. split; first done. apply _. Qed.
 Global Instance frame_idx_bor_own p i q1 q2 q :
-    FrameFractionalQp q1 q2 q →
-    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
+  FrameFractionalQp q1 q2 q →
+  Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
 (* FIXME: somehow Φ gets inferred wrong here. *)
 Proof. apply: (frame_fractional _ _ _ (λ q, idx_bor_own q i)%I). Qed.
 
-- 
GitLab