From 150070c61cf5e5b2e59da8b43d6e85de05c463d7 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 23 Jul 2021 15:58:17 +0200
Subject: [PATCH] Also review Iris instances outside [frame_instances]

---
 iris/bi/lib/fractional.v              | 2 +-
 iris/program_logic/total_weakestpre.v | 2 +-
 iris/program_logic/weakestpre.v       | 2 +-
 iris/proofmode/monpred.v              | 2 +-
 iris_heap_lang/derived_laws.v         | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 5c33516a9..05dee6eea 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -181,7 +181,7 @@ Section fractional.
   Global Instance 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.
+    Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 3b8c9d06c..d33ca14eb 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -284,7 +284,7 @@ Section proofmode_classes.
 
   Global Instance frame_twp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
+    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]) | 2.
   Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 59fbded04..22b5565f0 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -366,7 +366,7 @@ Section proofmode_classes.
 
   Global Instance frame_wp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
+    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 7073ed8d2..bc90575ed 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -364,7 +364,7 @@ Qed.
 
 (* Framing. *)
 Global Instance frame_monPred_at_enter p i 𝓡 P 𝓠 :
-  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠.
+  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠 | 2.
 Proof. intros. done. Qed.
 Global Instance frame_monPred_at_here p P i j :
   IsBiIndexRel i j → FrameMonPredAt p j (P i) P emp | 0.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 66a870aa5..f1627aa09 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -73,7 +73,7 @@ Qed.
 
 Global Instance array_cons_frame l dq v vs R Q :
   Frame false R (l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs) Q →
-  Frame false R (l ↦∗{dq} (v :: vs)) Q.
+  Frame false R (l ↦∗{dq} (v :: vs)) Q | 2.
 Proof. by rewrite /Frame array_cons. Qed.
 
 Lemma update_array l dq vs off v :
-- 
GitLab