From 1512b20a1b19ff18b97f654f74d80d33cb1b17c1 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 17 Jun 2025 14:51:23 +0200 Subject: [PATCH] Remove redundant notation reservation Those are already reserved, since forever, in bigop.v in mathcomp. Rereserving them only makes it impossible to change anything on mathcomp side. --- finmap.v | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/finmap.v b/finmap.v index 7d42a24..9484849 100644 --- a/finmap.v +++ b/finmap.v @@ -338,22 +338,6 @@ Reserved Notation "[ 'f' 'setval' x : A | P ]" Reserved Notation "[ 'f' 'setval' x : A | P & Q ]" (at level 0, x at level 99, format "[ 'f' 'setval' x : A | P & Q ]"). -Reserved Notation "\bigcup_ ( i <- r | P ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \bigcup_ ( i <- r | P ) '/ ' F ']'"). -Reserved Notation "\bigcup_ ( i <- r ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \bigcup_ ( i <- r ) '/ ' F ']'"). -Reserved Notation "\bigcup_ ( i | P ) F" - (at level 41, F at level 41, i at level 50, - format "'[' \bigcup_ ( i | P ) '/ ' F ']'"). -Reserved Notation "\bigcup_ ( i 'in' A | P ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \bigcup_ ( i 'in' A | P ) '/ ' F ']'"). -Reserved Notation "\bigcup_ ( i 'in' A ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \bigcup_ ( i 'in' A ) '/ ' F ']'"). - Reserved Notation "{fmap T }" (at level 0, format "{fmap T }"). Reserved Notation "x .[ k <- v ]" (left associativity, format "x .[ k <- v ]").