In current master we get a somewhat weird set of warnings when using the deprecated :>
syntax for subclass instances after the merge of https://github.com/coq/coq/pull/16230.
for instance,
Class Foo := {}.
Class Bar := {
foo :> Foo;
}.
results in
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]
that is, we get two warnings when I would have only expected one (the second one)
@Pierre Roux @Ali Caglayan is this the intended behaviour?
in particular the first warning is not emitted when using the ::
syntax (and it has an export semantics, kind of contradicting the warning)
Indeed, I should probably remove the first warning, it's now pretty redundant. Will open a PR.
@Pierre-Marie Pédrot here it is: https://github.com/coq/coq/pull/16331
Last updated: May 28 2023 at 16:30 UTC