diff --git a/theories/mapset.v b/theories/mapset.v
index 798f9761aa022431421a9e4bfa680ddb85dcbac2..5dc34e4038451e83d85821e0f8106f6fa83abafe 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -8,8 +8,9 @@ From stdpp Require Import options.
 locally (or things moved out of sections) as no default works well enough. *)
 Unset Default Proof Using.
 
-Record mapset (M : Type → Type) : Type :=
-  Mapset { mapset_car: M (unit : Type) }.
+Record mapset' (M : Type) : Type :=
+  Mapset { mapset_car: M }.
+Notation mapset M := (mapset' (M unit)).
 Global Arguments Mapset {_} _ : assert.
 Global Arguments mapset_car {_} _ : assert.