I just noticed a change from coq-8.12+mathcomp-1.11 to coq-8.13.1+mathcomp-1.12:

```
Goal forall (T : finType) (p : pred T) (A : {set sig p}),
val @: A \subset setT.
move=> T p A. rewrite /=.
```

now yields

```
[set (@sval) T (fun x : T => p x) x | x in A] \subset [set: T]
```

while it used to display as

```
[set sval x | x in A] \subset [set: T]
```

So it looks like the `sval`

notations are no longer working correctly. Is this a known issue?

It's not known to me, and it was not reported on github, please proceed.

FYI these are a few of the many changes in 8.13 w.r.t. notations:

- Changed: Redeclaring a notation also reactivates its printing rule; in particular a second Import of the same module reactivates the printing rules declared in this module. In theory, this leads to changes in behavior for printing. However, this is mitigated in general by the adoption in #12986 of a priority given to notations which match a larger part of the term to print (#12984, fixes #7443 and #10824, by Hugo Herbelin).
- Changed: Use of notations for printing now gives preference to notations which match a larger part of the term to abbreviate (#12986, by Hugo Herbelin).
- Changed: Scope information is propagated in indirect applications to a reference prefixed with @; this covers for instance the case r.(@p) t where scope information from p is now taken into account for interpreting t (#12685, by Hugo Herbelin).

CC @Hugo Herbelin

Given that the notation is part of ` Coq.ssr.ssrfun`

, I assume this should go into the Coq bug tracker, right?

Last updated: Jun 14 2024 at 18:01 UTC