diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 1071f99732248863931bdd804bcd2f429aaf2580..211b5c063b1fbc5e904c0191355c66fd0e4e251f 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import base_logic.
+Import stdpp.list. (* Make sure we use those names. FIXME: remove when we drop Coq 8.9 support. *)
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.