From 4b2f81cc361195dda0a839f92b374aebf1c99f09 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Nov 2016 15:39:40 +0100
Subject: [PATCH] Optimize dependencies of algebra/auth.
---
algebra/auth.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/algebra/auth.v b/algebra/auth.v
index da3d67f85..d2311b0d5 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.
--
GitLab