From a1abaf74772da06d53303352a13c92653da4f841 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 4 Jun 2023 17:59:27 +0200
Subject: [PATCH] reproducer for Coq bug

---
 iris/base_logic/lib/gen_heap.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 41f23cb4e..1bb7a7db1 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -188,10 +188,16 @@ Section gen_heap.
   Proof. rewrite mapsto_unseal. apply ghost_map_elem_persist. Qed.
 
   (** Framing support *)
+
+Typeclasses Opaque mapsto.
+Set Typeclasses Debug.
+Set Typeclasses Debug Verbosity 2.
+
   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.
-  Proof. apply: frame_fractional. Qed.
+  Proof.
+Fail apply: frame_fractional. Qed.
 
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
-- 
GitLab