Skip to content

Remove redundant `%I` scopes in definitions.

Robbert Krebbers requested to merge ci/robbert/I into master

This is a follow up of !456 (comment 51710)

Many uses of the %I scopes in iProp definitions are redundant. This MR removes all those that I could find.

Merge request reports