From 5d8dd9807474184d6f6efd955ef29aab6f60f3f5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Mar 2021 14:03:20 +0100
Subject: [PATCH] Ralf's suggested singleton notation.
---
theories/base.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base.v b/theories/base.v
index 2b00af03..8e2f922f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -866,7 +866,7 @@ Notation "{[ x ; y ; .. ; z ]}" :=
(union .. (union (singleton x) (singleton y)) .. (singleton z))
(at level 1) : stdpp_scope.
-Notation "+{[ x ; y ; .. ; z ]}" :=
+Notation "{[ x ;+ y ;+ .. ;+ z ]}" :=
(disj_union .. (disj_union (singleton x) (singleton y)) .. (singleton z))
(at level 1) : stdpp_scope.
--
GitLab