diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v index 8273c0797a3940270cf051043ae2a403deb5768a..5eba9f038fa85248333233cf78eef5d888ed7a14 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].