From c361b65175594a9c090b6d10348c55dc019c9908 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2022 09:33:20 +0100
Subject: [PATCH] Avoid universe constraints for `mapset`.

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

diff --git a/theories/mapset.v b/theories/mapset.v
index 798f9761..5dc34e40 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -8,8 +8,9 @@ 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) }.
+Record mapset' (M : Type) : Type :=
+  Mapset { mapset_car: M }.
+Notation mapset M := (mapset' (M unit)).
 Global Arguments Mapset {_} _ : assert.
 Global Arguments mapset_car {_} _ : assert.
 
-- 
GitLab