Commit 4b2f81cc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Optimize dependencies of algebra/auth.

parent c285069d
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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment