Use `#[local] field ::` to make `inG` instances local
Now that support for Coq 8.17 has been dropped, we can make use of #[local] field ::
in Class
declarations which by default appears to be . This would be a better fix for !780 (merged)Local
See also !1030 (merged)