Skip to content

Improve warning for nonuniform coercions #17713

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
proux01 wants to merge 1 commit into from
Closed

Improve warning for nonuniform coercions #17713

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion doc/sphinx/addendum/implicit-coercions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,7 +205,7 @@ Coercion Classes

The inferred target class of the coercion differs from the one specified.

.. warn:: @qualid does not respect the uniform inheritance condition.
.. warn:: @qualid does not respect the uniform inheritance condition. Use the '#[nonuniform]' attribute to silence this warning (available since Coq 8.16.0).

The :ref:`test for ambiguous coercion paths <ambiguous-paths>`
may yield false positives involving the coercion :token:`qualid`.
Expand Down
5 changes: 3 additions & 2 deletions test-suite/output/bug_5222.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,9 @@
============================
True = (nil : T1 nat)
File "./output/bug_5222.v", line 16, characters 2-40:
Warning: C2 does not respect the uniform inheritance condition.
[uniform-inheritance,coercions,default]
Warning: C2 does not respect the uniform inheritance condition. Use the
'#[nonuniform]' attribute to silence this warning (available since Coq
8.16.0). [uniform-inheritance,coercions,default]
1 goal

============================
Expand Down
10 changes: 6 additions & 4 deletions test-suite/output/coercions_nonuniform.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
File "./output/coercions_nonuniform.v", line 22, characters 0-21:
Warning: f does not respect the uniform inheritance condition.
[uniform-inheritance,coercions,default]
Warning: f does not respect the uniform inheritance condition. Use the
'#[nonuniform]' attribute to silence this warning (available since Coq
8.16.0). [uniform-inheritance,coercions,default]
File "./output/coercions_nonuniform.v", line 55, characters 0-17:
Warning: f' does not respect the uniform inheritance condition.
[uniform-inheritance,coercions,default]
Warning: f' does not respect the uniform inheritance condition. Use the
'#[nonuniform]' attribute to silence this warning (available since Coq
8.16.0). [uniform-inheritance,coercions,default]
File "./output/coercions_nonuniform.v", line 71, characters 7-17:
The command has indeed failed with message:
This command does not support this attribute: nonuniform.
Expand Down
4 changes: 3 additions & 1 deletion vernac/comCoercion.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -299,7 +299,9 @@ let warn_uniform_inheritance =
CWarnings.create ~name:"uniform-inheritance" ~category:CWarnings.CoreCategories.coercions
(fun g ->
Printer.pr_global g ++
strbrk" does not respect the uniform inheritance condition.")
strbrk" does not respect the uniform inheritance condition. \
Use the '#[nonuniform]' attribute to silence this warning \
(available since Coq 8.16.0).")

let add_new_coercion_core coef stre poly ~nonuniform ~reversible source target isid : unit =
check_source source;
Expand Down