diff --git a/theories/examples/rcu.v b/theories/examples/rcu.v
index 21611f5d9a6c4889a4de662873bc43fe1893e059..f702540faa84f5e95449ed06aba6cc12189fd12d 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.