diff options
| author | Pierre-Marie Pédrot | 2018-06-12 17:02:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-28 10:27:59 +0100 |
| commit | 8cdaa1b5c485ed351f9b3bf212ec5d88f8561908 (patch) | |
| tree | 7377c112460a11b4432f7bf0f9ac75a772be688b | |
| parent | aeca986089d005054496ed4bcf1b920e8fa02173 (diff) | |
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.
| -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 -> |