diff --git a/algebra/auth.v b/algebra/auth.v index da3d67f85b237d89bef0c6c9220592c0ceb1f4b1..d2311b0d59ff48cb5be48bfefffadc54bbce00c4 100644 --- a/algebra/auth.v +++ b/algebra/auth.v @@ -1,6 +1,6 @@ From iris.algebra Require Export excl local_updates. From iris.base_logic Require Import base_logic. -From iris.proofmode Require Import class_instances. +From iris.proofmode Require Import classes. Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }. Add Printing Constructor auth.