Stream: math-comp devs

Topic: regression with `sval` notaton (and maybe others)


view this post on Zulip Christian Doczkal (Mar 11 2021 at 09:57):

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?

view this post on Zulip Cyril Cohen (Mar 11 2021 at 13:40):

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

view this post on Zulip Enrico Tassi (Mar 11 2021 at 14:04):

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

CC @Hugo Herbelin

view this post on Zulip Christian Doczkal (Mar 11 2021 at 14:26):

Given that the notation is part of Coq.ssr.ssrfun, I assume this should go into the Coq bug tracker, right?


Last updated: Aug 11 2022 at 03:02 UTC