Merge branch 'robbert/mapset_universe' into 'master'

Avoid universe bumps of `gset`/`mapset` (fixes #134)

Closes #134

See merge request iris/stdpp!370

CHANGELOG.md

 This file lists "large-ish" changes to the std++ Coq library, but not every
 API-breaking change is listed.
 
+## std++ master
+
+- Make sure that `gset` and `mapset` do not bump the universe.
+
 ## std++ 1.7.0 (2022-01-22)
 
 Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain

tests/universes.ref

+gmap Z Z : Set
+     : Set
+gset Z : Set
+     : Set

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).

theories/mapset.v

@@ -8,8 +8,14 @@ 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) }.
+(** Given a type of maps [M : Type → Type], we construct sets as [M ()], i.e.,
+maps with unit values. To avoid unnecessary universe constraints, we first
+define [mapset' Munit] with [Munit : Type] as a record, and then [mapset M] with
+[M : Type → Type] as a notation. See [tests/universes.v] for a test case that
+fails otherwise. *)
+Record mapset' (Munit : Type) : Type :=
+  Mapset { mapset_car: Munit }.
+Notation mapset M := (mapset' (M unit)).
 Global Arguments Mapset {_} _ : assert.
 Global Arguments mapset_car {_} _ : assert.