diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index fd8e56476b6feee2e4f9b7ae89fb7461eaeb708a..9dadb62cdfcf3f5498ec78aac6089bfa1ec7e991 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -1,6 +1,6 @@
 From reloc Require Import reloc lib.lock.
 From iris.algebra Require Import numbers csum excl auth list gmap gset.
-From iris.bi.lib Require Export fixpoint.
+From iris.bi.lib Require Export fixpoint_mono.
 
 From reloc.examples.folly_queue Require Import
     set turnSequencer singleElementQueue CG_queue mpmcqueue.