diff --git a/theories/bsets.v b/theories/bset.v
similarity index 100%
rename from theories/bsets.v
rename to theories/bset.v
diff --git a/theories/co_pset.v b/theories/coPset.v
similarity index 100%
rename from theories/co_pset.v
rename to theories/coPset.v
diff --git a/theories/gmap.v b/theories/gmap.v
index b9cd019c7f81a5d7771fadd4aa1a3b8d0a6fc1eb..88f62e36e4a4dff78a3cd68c564852288bd80b33 100644
--- a/theories/gmap.v
+++ b/theories/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 stdpp Require Export countable fin_maps fin_map_dom.
-From stdpp Require Import pmap mapset sets.
+From stdpp 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/theories/sets.v b/theories/set.v
similarity index 100%
rename from theories/sets.v
rename to theories/set.v