diff options
| -rw-r--r-- | doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst | 5 | ||||
| -rw-r--r-- | vernac/g_proofs.mlg | 11 |
2 files changed, 15 insertions, 1 deletions
diff --git a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst new file mode 100644 index 0000000000..d2af6a4ca7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + Deprecated the declaration of arbitrary terms as hints. Global + references are now mandatory. + (`#7791 <https://github.com/coq/coq/pull/7791>`_, + by Pierre-Marie Pédrot). diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 03dfc576a1..596b04f7e3 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -43,6 +43,13 @@ let warn_deprecated_unfocus = CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" (fun () -> Pp.strbrk "The Unfocus command is deprecated") +let warn_deprecated_hint_constr = + CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + (fun () -> + Pp.strbrk + "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" + ) + } (* Proof commands *) @@ -107,7 +114,9 @@ GRAMMAR EXTEND Gram ] ]; reference_or_constr: [ [ r = global -> { HintsReference r } - | c = constr -> { HintsConstr c } ] ] + | c = constr -> + { warn_deprecated_hint_constr ~loc (); + HintsConstr c } ] ] ; hint: [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> |