From 04b066bcc389ffeb9cb35cd38b7005dd7fa44a6f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 20 Mar 2022 01:22:37 +0100
Subject: [PATCH] Make cinvG class a record

---
 iris/base_logic/lib/cancelable_invariants.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 8273c0797..5eba9f038 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class cinvG Σ := cinv_inG : inG Σ fracR.
+Class cinvG Σ := { cinv_inG : inG Σ fracR }.
 Local Existing Instance cinv_inG.
 
 Definition cinvΣ : gFunctors := #[GFunctor fracR].
-- 
GitLab