diff --git a/_CoqProject b/_CoqProject
index 7f98bf17f3e13429e71745dabdb393d5379a9dd4..000e00dbfe4bcaefb1e35e43c28e0744265d27a5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,7 @@
 -Q . iris
 prelude/option.v
 prelude/fin_map_dom.v
-prelude/bsets.v
+prelude/bset.v
 prelude/fin_maps.v
 prelude/vector.v
 prelude/pmap.v
@@ -28,9 +28,9 @@ prelude/finite.v
 prelude/numbers.v
 prelude/nmap.v
 prelude/zmap.v
-prelude/co_pset.v
+prelude/coPset.v
 prelude/lexico.v
-prelude/sets.v
+prelude/set.v
 prelude/decidable.v
 prelude/list.v
 prelude/error.v
diff --git a/algebra/sts.v b/algebra/sts.v
index 7950bf8cd6d86e902b095eadae399e52c6c64539..5be1a65749a34db099c0f1ab2de55c3b4f946ba4 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export sets.
+From iris.prelude Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
 Local Arguments valid _ _ !_ /.
diff --git a/prelude/bsets.v b/prelude/bset.v
similarity index 100%
rename from prelude/bsets.v
rename to prelude/bset.v
diff --git a/prelude/co_pset.v b/prelude/coPset.v
similarity index 100%
rename from prelude/co_pset.v
rename to prelude/coPset.v
diff --git a/prelude/gmap.v b/prelude/gmap.v
index d72514bc28ad831b5291ab7115d55834aee28abf..bf74baaafa5a49f93f2384d51016fa85080e2e59 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -3,7 +3,7 @@
 (** This file implements finite maps and finite sets with keys of any countable
 type. The implementation is based on [Pmap]s, radix-2 search trees. *)
 From iris.prelude Require Export countable fin_maps fin_map_dom.
-From iris.prelude Require Import pmap mapset sets.
+From iris.prelude Require Import pmap mapset set.
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
diff --git a/prelude/sets.v b/prelude/set.v
similarity index 100%
rename from prelude/sets.v
rename to prelude/set.v
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index ee59788b16cd3cbfff5a1fd16605e836d93c46c2..02e2a8dd6ec13c99ecde21d499b38c258b7fa19c 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export countable co_pset.
+From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
 
 Definition namespace := list positive.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index df3207507cf44a982b4b09e12e125593ff33f1af..7df7810618fe3710ac4653ea47238d71d3c7f396 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export co_pset.
+From iris.prelude Require Export coPset.
 From iris.algebra Require Export upred_big_op.
 From iris.program_logic Require Export model.
 From iris.program_logic Require Import ownership wsat.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 0392bd540d540693f8d5f132c8faa2e6afe28f3b..8e818b8c32e404082ef0437518b669a78a645f6d 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export co_pset.
+From iris.prelude Require Export coPset.
 From iris.program_logic Require Export model.
 From iris.algebra Require Export cmra_big_op cmra_tactics.
 Local Hint Extern 10 (_ ≤ _) => omega.