From 7baccddd441cd8fa12580dc858ec416aee9cd4a2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2022 09:41:21 +0100
Subject: [PATCH] Some documentation about `mapset`.

---
 theories/mapset.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/theories/mapset.v b/theories/mapset.v
index 5dc34e40..c1222987 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -8,8 +8,13 @@ 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 :=
-  Mapset { mapset_car: M }.
+(** Given a type of maps [M : Type → Type], we constructs 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.
-- 
GitLab