Skip to content
GitLab

Remove redundant `%I` scopes in definitions.

Merged 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.