The image notation (the one with the @ and the backquote) keeps on printing as `[set E | x in A]`

. Was this intended or is my setting wrong?

It is defined as an `only parsing`

notation https://github.com/math-comp/analysis/blob/master/theories/classical_sets.v#L291 so I guess this is expected.

the printing notation being https://github.com/math-comp/analysis/blob/master/theories/classical_sets.v#L215 (I don't know how Coq would behave if both notations were available for printing).

Thank you! I put an entry in the FAQ for me to remember. ^_^

Last updated: Jun 25 2024 at 17:02 UTC