silence fewer warnings, add comment about overwriting notation

@robbertkrebbers could you expand the comment to explain why we are doing this? Seems rather unfortunate.

@robbertkrebbers can I merge this?

The question is why do we do:

Notation "x - y" := (x + -y) : Qc_scope.

By default, Coq interprets x - y as something like Qc_minus, a definition which expands to the above. Since I always ended up unfolding that def first, I decided to just change the notation.

@robbertkrebbers can I merge this?

Sure.

Since I always ended up unfolding that def first, I decided to just change the notation.

I am not convinced that is a good enough justification for such an invasive change. Basically this should be listed in the "global side-effects" section, because that's what it is.

Feel free to undo the change and see if that breaks much.

added 1 commit

• 88e16c68 - do not override notation

Compare with previous version

I removed the notation and fixed std++. Iris still compiles without changes.

This makes std++ entirely warning-free, even with Coq 8.9.

Thanks. LGTM.

mentioned in commit 9e503f1a

merged