diff options
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 -> |