Backport PR coq#16252: note since when the things recommended in a de…

…precation note are supported
ppedrot · Jul 4, 2022 · 1534e3f · 1534e3f
2 parents ffcc588 + 49875ff
commit 1534e3f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/tactics/autorewrite.ml b/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

diff --git a/vernac/classes.ml b/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