From 9de9e04a6cb06ac2aac7a20b3c73e7f61d2c542d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 9 Jun 2023 13:04:20 +0200 Subject: [PATCH] Advertize the nonuniform attribute for coercions --- doc/sphinx/addendum/implicit-coercions.rst | 2 +- test-suite/output/bug_5222.out | 5 +++-- test-suite/output/coercions_nonuniform.out | 10 ++++++---- vernac/comCoercion.ml | 4 +++- 4 files changed, 13 insertions(+), 8 deletions(-) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index a4084b47b129..400878d6decb 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -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 ` may yield false positives involving the coercion :token:`qualid`. diff --git a/test-suite/output/bug_5222.out b/test-suite/output/bug_5222.out index bb357f075d49..dbbebde3d49f 100644 --- a/test-suite/output/bug_5222.out +++ b/test-suite/output/bug_5222.out @@ -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 ============================ diff --git a/test-suite/output/coercions_nonuniform.out b/test-suite/output/coercions_nonuniform.out index 3817b89621b7..6d5cc3663898 100644 --- a/test-suite/output/coercions_nonuniform.out +++ b/test-suite/output/coercions_nonuniform.out @@ -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. diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 3d2fe3c80057..d79eb1f3c078 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -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;