From 8cdaa1b5c485ed351f9b3bf212ec5d88f8561908 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 12 Jun 2018 17:02:34 +0200 Subject: Deprecating the declaration of arbitrary terms as hints. We restrict hints to be global references, so as to further simplify the implementation. Allowing arbitrary terms makes it difficult or expensive to handle properly some actions like universe contexts or hint equality. Ultimately, the IsConstr constructor for hints should also be removed. --- .../07-commands-and-options/7791-deprecate-hint-constr.rst | 5 +++++ vernac/g_proofs.mlg | 11 ++++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst 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 `_, + 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 -> -- cgit v1.2.3