Let compilation under Coq 8.17 succeed without warnings.
All threads resolved!
All threads resolved!
Compare changes
Files
3+ 1
− 1
@@ -44,7 +44,7 @@ Global Unset Transparent Obligations.
Warning: 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]Since we support Coq versions before 8.17, I just suppress these warnings using -future-coercion-class-field
Variants of:
Warning: Notation N.div_lt_upper_bound is deprecated since 8.17.
Use Div0.div_lt_upper_bound instead.
[deprecated-syntactic-definition,deprecated]See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Backwards.20compatibility.20w.2Er.2Et.2E.20Div0.20without.20warnings for the workaround that has been implemented.
File "./stdpp/base.v", line 47, characters 0-27:
Warning: The default and global localities for this command outside sections
are currently equivalent to the combination of the standard meaning of
"global" (as described in the reference manual), "export" and re-exporting
for every surrounding module. It will change to just "global" (with the
meaning used by the "Set" command) in a future release.
To preserve the current meaning in a forward compatible way, use the
attribute "#[global,export]" and repeat the command with just "#[export]" in
any surrounding modules. If you are fine with the change of semantics,
disable this warning. [deprecated-tacopt-without-locality,deprecated]This is about Obligation Tactic := idtac.
Maybe it should be Export, but that would be inconsistent with other choices we make Global. Since making it Export actually changes things, we should investigate that in a separate MR if we deem it necessary.