diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v index e73a3db30b34006a0d79433f3eed4b87406a2d09..3320476460e984564768221c7f9da4816a1f28a8 100644 --- a/theories/algebra/agree.v +++ b/theories/algebra/agree.v @@ -1,7 +1,6 @@ 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 _ _ _ !_ /.