Skip to content

Make `gset` a `Definition` instead of `Notation`.

Robbert Krebbers requested to merge robbert/gset_definition into master

I mainly did do this because it often confused me that when using Set Printing All occurrences of gset are turned into mapset ....

However, it turned out this also has a positive effect on performance. On my machine, compilation of LambdaRust went from 34m2s to 33m1s, so that's an improvement of 3%. It had no significant effect on compilation times of Iris itself.

Merge request reports