diff --git a/CHANGELOG.md b/CHANGELOG.md index 0d3f57919eeb638fedc5f49c67d174b33b38b6b2..4b39ffc11365b45966c44230dc8e9b8a5c67bae9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,10 @@ 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 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). diff --git a/theories/mapset.v b/theories/mapset.v index 798f9761aa022431421a9e4bfa680ddb85dcbac2..41119302492e06beebd86392a2a1ff26ea8ac689 100644 --- a/theories/mapset.v +++ b/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.