From 93f9452cd95ec478bed2f798afa2e748f2dd0a9b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Dec 2021 23:12:28 +0100
Subject: [PATCH] to_frac_agree is deliberately transparent
---
iris/algebra/lib/dfrac_agree.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
index 251d48866..388fd6dbc 100644
--- a/iris/algebra/lib/dfrac_agree.v
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -11,6 +11,7 @@ Global Instance: Params (@to_dfrac_agree) 2 := {}.
[to_frac_agree] and appropriate lemmas. *)
Definition to_frac_agree {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A :=
to_dfrac_agree (DfracOwn q) a.
+Global Instance: Params (@to_frac_agree) 2 := {}.
Section lemmas.
Context {A : ofe}.
@@ -125,3 +126,4 @@ Section lemmas.
End lemmas.
Typeclasses Opaque to_dfrac_agree.
+(* to_frac_agree is deliberately transparent to reuse the to_dfrac_agree instances *)
--
GitLab