diff options
| author | Pierre-Marie Pédrot | 2020-02-28 10:29:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-28 10:32:25 +0100 |
| commit | eabde14cce66553f9ba7b583507af51973ded850 (patch) | |
| tree | 48ea0b19afb5936b92fed34d4dd880668b03d184 | |
| parent | 3034319a2f52baeca172a33eb98b20b3e559201f (diff) | |
Move the warning code out of the parser.
| -rw-r--r-- | tactics/hints.ml | 11 | ||||
| -rw-r--r-- | vernac/g_proofs.mlg | 11 |
2 files changed, 11 insertions, 11 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 86aa046586..731792e34e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1325,6 +1325,13 @@ let project_hint ~poly pri l2r r = let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) +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" + ) + let interp_hints ~poly = fun h -> let env = Global.env () in @@ -1349,7 +1356,9 @@ let interp_hints ~poly = | HintsReference c -> let gr = global_with_alias c in (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> (PathAny, poly, f poly c) + | HintsConstr c -> + let () = warn_deprecated_hint_constr () in + (PathAny, poly, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 596b04f7e3..03dfc576a1 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -43,13 +43,6 @@ 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 *) @@ -114,9 +107,7 @@ GRAMMAR EXTEND Gram ] ]; reference_or_constr: [ [ r = global -> { HintsReference r } - | c = constr -> - { warn_deprecated_hint_constr ~loc (); - HintsConstr c } ] ] + | c = constr -> { HintsConstr c } ] ] ; hint: [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> |