diff --git a/tests/universes.ref b/tests/universes.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e9db4532ac513fddc994f3e78a37befb7fa4e06c
--- /dev/null
+++ b/tests/universes.ref
@@ -0,0 +1,4 @@
+gmap Z Z : Set
+     : Set
+gset Z : Set
+     : Set
diff --git a/tests/universes.v b/tests/universes.v
new file mode 100644
index 0000000000000000000000000000000000000000..a6dcd8d9820dc2cbf9dd52e44796bc984bb03611
--- /dev/null
+++ b/tests/universes.v
@@ -0,0 +1,7 @@
+From stdpp Require Import gmap.
+
+(** Make sure that [gmap] and [gset] do not bump the universe. Since [Z : Set],
+the types [gmap Z Z] and [gset Z] should have universe [Set] too. *)
+
+Check (gmap Z Z : Set).
+Check (gset Z : Set).