Class Foo := {}.

Class Bar := {
  foo :> Foo;
}.

The default value for field instance locality is currently "global", but
is scheduled to change in a future release. For the time being, adding
field instances without specifying an explicit locality attribute is
therefore deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and #[export] depending
on your choice. For example: "Class foo := { #[export] field :: bar }."
[deprecated-field-instance-without-locality,deprecated]
A coercion will be introduced instead of an instance in future versions
when using ':>' in 'Class' declarations. Replace ':>' with '::' (or use
'#[global] Existing Instance field.' for compatibility with Coq < 8.17).
Beware that the default locality for '::' is #[export], as opposed to
#[global] for ':>' currently. Add an explicit #[global] attribute to the
field if you need to keep the current behavior. For example: "Class foo
:= { #[global] field :: bar }." [future-coercion-class-field,records]