Merge PR #16252: note since when the things recommended in a deprecation note are supported

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

Author: coqbot-app[bot]

tactics/autorewrite.ml

@@ -263,7 +263,7 @@ let warn_deprecated_hint_rewrite_without_locality =
     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: \
-    \"#[export] Hint Rewrite foo : bar.\"")
+    \"#[export] Hint Rewrite foo : bar.\" This is supported since Coq 8.14.")
 
 let default_hint_rewrite_locality () =
   if Global.sections_are_opened () then Hints.Local

vernac/classes.ml

@@ -40,7 +40,8 @@ let warn_deprecated_tc_transparency_without_locality =
    sections 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: \"#[export] Typeclasses Transparent foo.\"")
+   depending on your choice. For example: \"#[export] Typeclasses Transparent foo.\". \
+   This is supported since Coq 8.15.")
 
 let default_tc_transparency_locality () =
   if Global.sections_are_opened () then Hints.Local