From 5c98c9a8ed6b68f00a44a52c28e361f5e0874df2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Dec 2021 11:54:28 +0100
Subject: [PATCH] add Params
---
iris/algebra/lib/dfrac_agree.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
index e6ddd88c1..251d48866 100644
--- a/iris/algebra/lib/dfrac_agree.v
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -6,6 +6,7 @@ Definition dfrac_agreeR (A : ofe) : cmra := prodR dfracR (agreeR A).
Definition to_dfrac_agree {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A :=
(d, to_agree a).
+Global Instance: Params (@to_dfrac_agree) 2 := {}.
(** To make it easier to work with the [Qp] version of this, we also provide
[to_frac_agree] and appropriate lemmas. *)
Definition to_frac_agree {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A :=
--
GitLab