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 /vernac | |
| 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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_proofs.mlg | 11 |
1 files changed, 10 insertions, 1 deletions
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 -> |