From 31de0c904dc791ced74da256a9e4bf88f624fef7 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 12 Jun 2023 09:44:18 +0200
Subject: [PATCH] More tweaks, add comment on hints

---
 iris/algebra/cmra.v   | 3 +++
 iris/algebra/csum.v   | 5 ++++-
 iris/algebra/excl.v   | 5 ++++-
 iris/bi/internal_eq.v | 3 +--
 iris/bi/lib/cmra.v    | 2 +-
 5 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 4b2789697..bd69ec9a8 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -637,6 +637,9 @@ Global Instance exclusive_id_free x : Exclusive x → IdFree x.
 Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
 End cmra.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
 Global Hint Extern 0 (?a ≼ ?a ⋅ _) => apply: cmra_included_l : core.
 Global Hint Extern 0 (?a ≼ _ ⋅ ?a) => apply: cmra_included_r : core.
 
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 47b946117..3a76de354 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -369,7 +369,10 @@ Proof.
 Qed.
 End cmra.
 
-Global Hint Extern 4 (_ ≼ CsumBot) => apply: CsumBot_included : core.
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ CsumBot) => apply: CsumBot_included : core.
 Global Arguments csumR : clear implicits.
 
 (* Functor *)
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index 7ffff44b8..94b792756 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -116,7 +116,10 @@ Lemma ExclBot_included ea : ea ≼ ExclBot.
 Proof. by exists ExclBot. Qed.
 End excl.
 
-Global Hint Extern 4 (_ ≼ ExclBot) => apply: ExclBot_included : core.
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ ExclBot) => apply: ExclBot_included : core.
 
 Global Arguments exclO : clear implicits.
 Global Arguments exclR : clear implicits.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 5041d5690..6a7eca83d 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -159,8 +159,7 @@ Section internal_eq_derived.
   Qed.
 
   Lemma csum_equivI {A B : ofe} (sx sy : csum A B) :
-    sx ≡ sy ⊣⊢
-              match sx, sy with
+    sx ≡ sy ⊣⊢ match sx, sy with
                | Cinl x, Cinl y => x ≡ y
                | Cinr x, Cinr y => x ≡ y
                | CsumBot, CsumBot => True
diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v
index 85b9abdc7..f3a8b9a20 100644
--- a/iris/bi/lib/cmra.v
+++ b/iris/bi/lib/cmra.v
@@ -57,7 +57,7 @@ Section internal_included_laws.
 
   Lemma internal_included_refl `{!CmraTotal A} (x : A) : ⊢@{PROP} x ≼ x.
   Proof. iExists (core x). by rewrite cmra_core_r. Qed.
-  Lemma internal_included_trans `{!CmraTotal A} (x y z : A) :
+  Lemma internal_included_trans {A} (x y z : A) :
     ⊢@{PROP} x ≼ y -∗ y ≼ z -∗ x ≼ z.
   Proof.
     iIntros "#[%x' Hx'] #[%y' Hy']". iExists (x' â‹… y').
-- 
GitLab