Skip to content

Commit 1512b20

Browse files
committed
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.
1 parent 054881a commit 1512b20

File tree

1 file changed

+0
-16
lines changed

1 file changed

+0
-16
lines changed

finmap.v

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -338,22 +338,6 @@ Reserved Notation "[ 'f' 'setval' x : A | P ]"
338338
Reserved Notation "[ 'f' 'setval' x : A | P & Q ]"
339339
(at level 0, x at level 99, format "[ 'f' 'setval' x : A | P & Q ]").
340340

341-
Reserved Notation "\bigcup_ ( i <- r | P ) F"
342-
(at level 41, F at level 41, i, r at level 50,
343-
format "'[' \bigcup_ ( i <- r | P ) '/ ' F ']'").
344-
Reserved Notation "\bigcup_ ( i <- r ) F"
345-
(at level 41, F at level 41, i, r at level 50,
346-
format "'[' \bigcup_ ( i <- r ) '/ ' F ']'").
347-
Reserved Notation "\bigcup_ ( i | P ) F"
348-
(at level 41, F at level 41, i at level 50,
349-
format "'[' \bigcup_ ( i | P ) '/ ' F ']'").
350-
Reserved Notation "\bigcup_ ( i 'in' A | P ) F"
351-
(at level 41, F at level 41, i, A at level 50,
352-
format "'[' \bigcup_ ( i 'in' A | P ) '/ ' F ']'").
353-
Reserved Notation "\bigcup_ ( i 'in' A ) F"
354-
(at level 41, F at level 41, i, A at level 50,
355-
format "'[' \bigcup_ ( i 'in' A ) '/ ' F ']'").
356-
357341
Reserved Notation "{fmap T }" (at level 0, format "{fmap T }").
358342
Reserved Notation "x .[ k <- v ]"
359343
(left associativity, format "x .[ k <- v ]").

0 commit comments

Comments
 (0)