From ea51b43ba10109c71288e0a8ab69300e93ffb8a8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 30 Sep 2021 21:37:58 -0400
Subject: [PATCH] perf experiment: dont make frame_fractional an instance

---
 iris/bi/lib/fractional.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 8a061d689..81552437d 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -194,7 +194,8 @@ Section fractional.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
 
-  Global Instance frame_fractional p R r Φ P q RES:
+  (* Not an instance because of performance; you can locally add it if you are willing to pay the cost. *)
+  Lemma frame_fractional p R r Φ P q RES:
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →
     Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
-- 
GitLab