From e87b3a26abfda7823cb8d99e956157cdc1e4877b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thibaut=20P=C3=A9rami?= <thibaut.perami@cl.cam.ac.uk>
Date: Wed, 18 Oct 2023 11:41:37 +0100
Subject: [PATCH] Allow patterns and type annotations in propset notation
---
stdpp/propset.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/stdpp/propset.v b/stdpp/propset.v
index 1ed3af52..5c829eb6 100644
--- a/stdpp/propset.v
+++ b/stdpp/propset.v
@@ -7,7 +7,7 @@ Add Printing Constructor propset.
Global Arguments PropSet {_} _ : assert.
Global Arguments propset_car {_} _ _ : assert.
Notation "{[ x | P ]}" := (PropSet (λ x, P))
- (at level 1, format "{[ x | P ]}") : stdpp_scope.
+ (at level 1, x at level 200 as pattern, format "{[ x | P ]}") : stdpp_scope.
Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
--
GitLab