From 6c174ea1d4fef70ae6bd15d5d0052680bfa87013 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jul 2022 14:34:50 +0200
Subject: [PATCH] Add comment.

---
 iris/base_logic/lib/later_credits.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 27433b31b..d63748060 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -105,6 +105,8 @@ Section later_credit_theory.
     rewrite lc_unseal /lc_def. apply _.
   Qed.
 
+  (** Make sure that the rule for [+] is used before [S], otherwise Coq's
+  unification applies the [S] hint too eagerly. See Iris issue #470. *)
   Global Instance from_sep_lc_add n m :
     FromSep (£ (n + m)) (£ n) (£ m) | 0.
   Proof.
-- 
GitLab