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 /tactics/hints.ml | |
| parent | 3034319a2f52baeca172a33eb98b20b3e559201f (diff) | |
Move the warning code out of the parser.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 11 |
1 files changed, 10 insertions, 1 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) = |