Mark ring morphisms as opaque.

This prevents Coq from unfolding IZR in ring_simplify and field_simplify.

This is a change of behavior for users of morphism rings, so they might have
to pass the postprocess option to Add Ring/Field if they want morphisms to be
automatically expanded.

There are two predefined morphisms in the standard library: IDphi (when
polynomial coefficients have the same type as constants) and gen_phiZ (when
the only available constants are 0 and 1). They are hardcoded as transparent.

0 files changed, 0 insertions, 0 deletions