From 1a42179046e274ae3406644fc04692432b77ef0d Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 15 Mar 2022 21:41:04 +0000 Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s) --- theories/mapset.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/mapset.v b/theories/mapset.v index c1222987..41119302 100644 --- a/theories/mapset.v +++ b/theories/mapset.v @@ -8,7 +8,7 @@ From stdpp Require Import options. locally (or things moved out of sections) as no default works well enough. *) Unset Default Proof Using. -(** Given a type of maps [M : Type → Type], we constructs sets as [M ()], i.e., +(** 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 -- GitLab