From c2556bbedf56ed61edecd6c758fc06db4611dab0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 20 Oct 2020 15:03:48 +0200
Subject: [PATCH] fix imports

---
 theories/base_logic/algebra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 21d496480..6c86be60b 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import cmra view auth agree csum list excl gmap lib.excl_auth lib.gmap_view.
-From iris.proofmode Require Import tactics.
+From iris.algebra Require Import cmra view auth agree csum list excl gmap.
+From iris.algebra.lib Require Import excl_auth gmap_view.
 From iris.base_logic Require Import bi derived.
 From iris Require Import options.
 
-- 
GitLab