From 38d04e99362e3d3a16eb1eb90254be0f6a8ea0a8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2022 09:35:23 +0100
Subject: [PATCH] Add tests for universe bumping of `gset`.

---
 tests/universes.ref | 4 ++++
 tests/universes.v   | 7 +++++++
 2 files changed, 11 insertions(+)
 create mode 100644 tests/universes.ref
 create mode 100644 tests/universes.v

diff --git a/tests/universes.ref b/tests/universes.ref
new file mode 100644
index 00000000..e9db4532
--- /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 00000000..a6dcd8d9
--- /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).
-- 
GitLab