From 6a09a8278a467b2aa537a0f91d716d1f6b82f6eb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Mar 2018 17:36:25 +0100
Subject: [PATCH] rcu: get rid of coqdep errors, at least

---
 theories/examples/rcu.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/examples/rcu.v b/theories/examples/rcu.v
index 21611f5d..f702540f 100644
--- a/theories/examples/rcu.v
+++ b/theories/examples/rcu.v
@@ -1,7 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth coPset.
-From iris.base_logic Require Import big_op.
 
 From igps Require Import notation malloc escrows repeat protocols bigop.
 From igps.gps Require Import shared plain fractional singlewriter recursive.
-- 
GitLab