Improving coding style
It would be a good idea to also enforce (via CI) the coding style improvements we have in Iris, here in the examples project:
-
no auto-generated names -
import "options" file everywhere that sets Default Goal Selector
-
Enforce Local
/Global
via ourcoq-lint.sh
Then we also should enable CI for MRs the same way we do for Iris.