Improve 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 -- mostly done, some files missing: -
logrel/stlc/fundamental.v
-
logrel/F_mu_ref_conc/unary/logrel.v
-
logrel/F_mu_ref_conc/binary/logrel.v
-
-
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.
Edited by Ralf Jung