diff options
| author | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
| commit | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (patch) | |
| tree | f4b84d2114aa4523aebf62f020ae46f4321fb10a /tactics | |
| parent | ba8e3caa31e464d1007c4ad54e8d70fd70ca3300 (diff) | |
| parent | eeb1d861551e25c6a92721334b3c9f36b7ebb012 (diff) | |
Merge PR #8987: Deprecate hint declaration/removal with no specified database
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 2f2d32e887..328d57c8a3 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1373,10 +1373,10 @@ let interp_hints poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints ~local dbnames0 h = - if String.List.mem "nocore" dbnames0 then +let add_hints ~local dbnames h = + if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); - let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in + assert (not (List.is_empty dbnames)); let env = Global.env() in let sigma = Evd.from_env env in match h with |