Skip to content

silence fewer warnings, add comment about overwriting notation

Ralf Jung requested to merge ralf/notation into master

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

Merge request reports