Skip to content
Snippets Groups Projects
Verified Commit 04b066bc authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Make cinvG class a record

parent b43f13c9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/base_logic/lib/cancelable_invariants.v
+ 1
− 1
View file @ 04b066bc
...@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Export invariants. ...@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.prelude Require Import options. From iris.prelude Require Import options.
Import uPred. Import uPred.
Class cinvG Σ := cinv_inG : inG Σ fracR. Class cinvG Σ := { cinv_inG : inG Σ fracR }.
Local Existing Instance cinv_inG. Local Existing Instance cinv_inG.
Definition cinvΣ : gFunctors := #[GFunctor fracR]. Definition cinvΣ : gFunctors := #[GFunctor fracR].
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment