From 610ed56460fc65a26e6b26159b70a93234477cd0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jul 2022 09:26:20 +0200
Subject: [PATCH] =?UTF-8?q?Tweak=20priority=20of=20proof=20mode=20instance?=
 =?UTF-8?q?s=20for=20=C2=A3.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This closes issue #470.
---
 iris/base_logic/lib/later_credits.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index acd0190cf..27433b31b 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -106,23 +106,23 @@ Section later_credit_theory.
   Qed.
 
   Global Instance from_sep_lc_add n m :
-    FromSep (£ (n + m)) (£ n) (£ m).
+    FromSep (£ (n + m)) (£ n) (£ m) | 0.
   Proof.
     by rewrite /FromSep lc_split.
   Qed.
   Global Instance from_sep_lc_S n :
-    FromSep (£ (S n)) (£ 1) (£ n).
+    FromSep (£ (S n)) (£ 1) (£ n) | 1.
   Proof.
     by rewrite /FromSep (lc_succ n).
   Qed.
 
   Global Instance into_sep_lc_add n m :
-    IntoSep (£ (n + m)) (£ n) (£ m).
+    IntoSep (£ (n + m)) (£ n) (£ m) | 0.
   Proof.
     by rewrite /IntoSep lc_split.
   Qed.
   Global Instance into_sep_lc_S n :
-    IntoSep (£ (S n)) (£ 1) (£ n).
+    IntoSep (£ (S n)) (£ 1) (£ n) | 1.
   Proof.
     by rewrite /IntoSep (lc_succ n).
   Qed.
-- 
GitLab