Add tests for universe bumping of `gset`.

38d04e99 · Robbert Krebbers · c361b651 · 38d04e99 · 38d04e99
Commit 38d04e99 authored 3 years ago by Robbert Krebbers
--- a/tests/universes.ref
+++ b/tests/universes.ref
+gmap Z Z : Set
+     : Set
+gset Z : Set
+     : Set
--- a/tests/universes.v
+++ b/tests/universes.v
+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).