Use Michocoq certified optimizer
In mi-cho-coq!53 (merged), a slightly extended version of the optimizer is certified. Albert's compiler should use it.
In mi-cho-coq!53 (merged), a slightly extended version of the optimizer is certified. Albert's compiler should use it.