From ed17518b5981e0bd0e7f4efa834b6939708922ea Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 Dec 2023 21:56:47 +0900 Subject: [PATCH] fix --- classical/classical_sets.v | 1 + 1 file changed, 1 insertion(+) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index a16b493e5..3bf3f9df8 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -55,6 +55,7 @@ From mathcomp Require Import mathcomp_extra boolp. (* | trivIset D F |==| F is a sequence of pairwise disjoint | *) (* | | | sets indexed over the domain D | *) (* *) +(* Details: *) (* ## Sets *) (* ``` *) (* set T == type of sets on T *)